Formal Specification of ML Programs

D. Sannella

Abstract: These notes were written to accompany lectures on program specification which formed part of a course on functional programming in ML. Functions can be specified using a specification language obtained by extending ML with (non-executable) first-order axioms. Simple inductive proofs suffice to show that an ML function satisfies such a specification. This approach can also be used to specify and verify larger programs built from smaller pieces using ML's modularisation facilities. Examples are used to illustrate the methods discussed.

LFCS report ECS-LFCS-86-15

Previous | Index | Next