The Specification Statement
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 more as it should be: 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 generalised 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.
Unable to display preview. Download preview PDF.