A Kernel Specification Formalism with Higher-Order Parameterisation

Donald Sannella, Andrzej Tarlecki

Research output: Chapter in Book/Report/Conference proceedingConference contribution


A specification formalism with parameterisation of an arbitrary order is presented. It is given a denotational-style semantics, accompanied by an inference system for proving that an object satisfies a specification. The inference system incorporates, but is not limited to, a clearly identified type-checking component. Special effort is made to carefully distinguish between parameterised specifications, which denote functions yielding classes of objects, and specifications of parameterised objects, which denote classes of functions yielding objects. To deal with both of these in a uniform framework, it was convenient to view specifications, which specify objects, as objects themselves, and to introduce a notion of a specification of specifications. The formalism includes the basic specification-building operations of the ASL specification language. This choice, however, is orthogonal to the new ideas presented. The formalism is also institution-independent, although this issue is not explicitly discussed at any length here.

Original languageEnglish
Title of host publicationRecent Trends in Data Type Specification
Subtitle of host publication7th Workshop on Specification of Abstact Data Types Wusterhausen/Dosse, Germany, April 17–20, 1990 Proceedings
PublisherSpringer-Verlag GmbH
Number of pages23
ISBN (Electronic)978-3-540-38416-8
ISBN (Print)978-3-540-54496-8
Publication statusPublished - 1991

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'A Kernel Specification Formalism with Higher-Order Parameterisation'. Together they form a unique fingerprint.

Cite this