SPECIFICATIONS‚ PROGRAMS AND IMPLEMENTATIONS
C.A.R. Hoare
Abstract
A specification is a predicate describing all observations permitted of the system specified. Specifications of complex systems can be constructed from specifications of their components by connectives defined in the predicate calculus. A program is just a predicate expressed using only a restricted subset of such connectives, codified as a programming language. An implementation of the programming language is a mechanism that will accept any predicate of the language, and then behave as described by it. Given a proposed model of an implementation it is desirable to prove that every program expressible in the language is consistent and complete with respect to the model; furthermore, there should be no program which logically implies all the others. These points are illustrated by the design of a very simple programming language, describing the interactions of concurrent processes. It is suggested that the design of a realistic programming language requires, and is worthy of, the skills of a mathematical logician.