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.


Natural Deduction Semantic Framework Program Fragment Weak Precondition Abstract Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Association for Computing Machinery 1988

Authors and Affiliations

  • Carroll Morgan

There are no affiliations available

Personalised recommendations