Toward formal development of ML programs: foundations and methodology - Preliminary version

Donald Sannella and Andrzej Tarlecki

Abstract: a formal methodology is presented for the systematic evolution of modular Standard ML programs from specifications by means of verified refinement steps, in the framework of the Extended ML specification language. Program development proceeds via a sequence of design (modular decomposition), coding and refinement steps. For each of these three kinds of steps, conditions are given which ensure the correctness of the result. These conditions seem to be as weak as possible under the constraint of being expressible as ``local'' interface matching requirements. Interfaces are only required to match up to behavioural equivalence, which is seen as vital to the use of data abstraction in program development.


Previous | Index | Next