Extended ML : An Institution-independent Framework for Formal Program Development

D. Sannella and A. Tarlecki

Abstract: The Extended ML specification language provides a framework for the formal stepwise development of modular programs in the Standard ML programming language from specifications. The object of this paper is to equip Extended ML with a semantics which is completely independent of the logical system used to write specifications, building on Goguen and Burstall's work on the notion of an institution as a formalisation of the concept of a logical system. One advantage of this is that it permits freedom in the choice of the logic used in writing specifications; an intriguing side-effect is that it enables Extended ML to be used to develop programs in languages other than Standard ML since we view programs as simply Extended ML specifications which happen to include only ``executable'' axioms. The semantics of Extended ML is defined in terms of the primitive specification-building operations of the ASL kernel specification language which itself has an institution-independent semantics.

It is not possible to give a semantics for Extended ML in an institutional framework without extending the notion of an institution; the new notion of an institution with syntax is introduced to provide an adequate foundation for this enterprise. An institution with syntax is an institution with three additions: the category of signatures is assumed to form a concrete category; an additional functor is provided which gives concrete syntactic representations of sentences; and a natural transformation associates these concrete objects with the ``abstract'' sentences they represent. We use the first addition to ``lift'' certain necessary set-theoretic constructions to the category of signatures, and the other two additions to deal with the low-level semantics of axioms.

LFCS report ECS-LFCS-86-16

Previous | Index | Next