Program Specification and Development in Standard ML

Abstract

An attempt is made to apply ideas about algebraic specification in the context of a programming language. Standard ML with modules is extended by allowing axioms in module interface specifications and in place of code. The resulting specification language, called Extended ML, is given a semantics based on the primitive specification-building operations of the kernel algebraic specification language ASL. Extended ML provides a framework for the formal development of programs from specifications by stepwise refinement, which is illustrated by means of a simple example. From its semantic basis Extended ML inherits complete independence from the logical system (institution) used to write specifications. This allows different styles of specification as well as different programming languages to be accommodated.