Specifications in an arbitrary institution

Donald Sannella, Andrzej Tarlecki

Research output: Contribution to journalArticlepeer-review

Abstract

A formalism for constructing and using axiomatic specifications in an arbitrary logical system is presented. This builds on the framework provided by Goguen and Burstall's work on the notion of an institution as a formalisation of the concept of a logical system for writing specifications. We show how to introduce free variables into the sentences of an arbitrary institution and how to add quantifiers which bind them. We use this foundation to define a set of primitive operations for building specifications in an arbitrary institution based loosely on those in the ASL kernel specification language. We examine the set of operations which results when the definitions are instantiated in institutions of total and partial first-order logic and compare these with the operations found in existing specification languages. We present proof rules which allow proofs to be conducted in specifications built using the operations we define. Finally, we introduce a simple mechanism for defining and applying parameterised specifications and briefly discuss the program development process.
Original languageEnglish
Pages (from-to)165 - 210
JournalInformation and Computation
Volume76
Issue number2-3
DOIs
Publication statusPublished - 1988

Fingerprint

Dive into the research topics of 'Specifications in an arbitrary institution'. Together they form a unique fingerprint.

Cite this