## A Study in the Foundations of Programming Methodology:
Specifications, Institutions, Charters and Parchments

**J.A. Goguen and R. Burstall**
*Abstract:* The theory of institutions formalizes the
intuitive notion of a ``logical system''. Institutions were
introduced (1) to support as much computer science as possible
*independently* of the underlying logical system, (2) to
facilitate the transfer of results (and artifacts such as theorem
provers) from one logical system to another, and (3) to permit
combining a number of different logical systems. In particular,
programming in-the-large (in the style of the Clear specification
language) is available for any specification or ``logical''
programming language based upon a suitable institution. Available
features include generic modules, module hierarchies, ``data
constraints'' (for data abstraction), and ``multiplex''
institutions (for combining multiple logical systems). The basic
components of an institution are: a category of signatures (which
generally provide symbols for constructing sentences); a set (or
category) of sigma-**sentences** for each signature sigma; a
category (or set) of sigma-models, for each sigma. The intuition of
the basic axiom for institutions is that *truth* (i.e.,
*satisfaction*) *is invariant under change of notation*.
This paper enriches institutions with sentence morphisms to model
proofs, and uses this to explicate the notion of a logical
programming language.

To ease constructing institutions, and to clarify various
notions, this paper introduces two further concepts. A
**charter** consists of an adjunction, a ``base'' functor, and a
``ground'' object; we show that ``chartering'' is a convenient way
to ``found'' institutions. **Parchments** provide a notion of
sentential syntax, and a simple way to ``write'' charters and thus
get institutions. Parchments capture the insight *that the syntax
of logic is an initial algebra*. Everything is illustrated with
the many-sorted equational institution. Parchments also explicate
the sense of finitude that is appropriate for specifications.
Finally, we introduce **generalized institutions**, which
generalize both institutions and Mayoh's ``galleries'', and we
introduce corresponding generalized charters and parchments.

*LFCS report ECS-LFCS-86-10*

Previous |

Index |

Next