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.
KeywordsNatural Deduction Semantic Framework Program Fragment Weak Precondition Abstract Program
Unable to display preview. Download preview PDF.