Simple Type Theory: Simple Steps Towards a Formal Specification

William M. Farmer and Martin v. Mohrenschildt

2004

Abstract

Engineers, particularly software engineers, need to know how to read
and write precise specifications.  Specifications are made precise by
expressing them in a formal mathematical language.  Simple type
theory, also as known as higher-order logic, is an excellent
educational and practical tool for creating and understanding formal
specifications.  It provides a better logical foundation for
specification than first-order logic and is a better introductory
specification language than industrial specification languages like
VDM-SL and Z.  For these reasons, we recommend that simple type theory
be incorporated into the undergraduate engineering curriculum.