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.
Previous | Index | Next An error occured whilst processing this directive