The specification statement

Abstract

Dijkstra's programming language is extended by specification statements , which specify parts of a program “yet to be developed.” A weakest precondition semantics is given for these statements so that the extended language has a meaning as precise as the original. The goal is to improve the development of programs, making it closer to manipulations within a single calculus. The extension does this by providing one semantic framework for specifications and programs alike: Developments begin with a program (a single specification statement) and end with a program (in the executable language). And the notion of refinement or satisfaction , which normally relates a specification to its possible implementations, is automatically generalized to act between specifications and between programs as well. A surprising consequence of the extension is the appearance of miracles : program fragments that do not satisfy Dijkstra's Law of the Excluded Miracle . Uses for them are suggested.