Formal models of stepwise refinements of programs
- 1 September 1986
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Computing Surveys
- Vol. 18 (3) , 231-276
- https://doi.org/10.1145/27632.28054
Abstract
Of the many ways to express program specifications, three of the most common are: as a pair of assertions, an input assertion and an output assertion; as a function mapping legal inputs to correct outputs; or as a relation containing the input/output pairs that are considered correct. The construction of programs consists of mapping a potentially complex specification into a program by recursively decomposing complex specifications into simpler ones. We show how this decomposition takes place in all three modes of specification and draw some conclusions on the nature of programming.Keywords
This publication has 24 references indexed in Scilit:
- Small programming exercises 8Science of Computer Programming, 1985
- Small programming exercises 7Science of Computer Programming, 1985
- Predicative programming Part ICommunications of the ACM, 1984
- Predicative programming Part IICommunications of the ACM, 1984
- A generalized control structure and its formal definitionCommunications of the ACM, 1983
- A Comparative Analysis of Functional CorrectnessACM Computing Surveys, 1982
- Guarded commands, nondeterminacy and formal derivation of programsCommunications of the ACM, 1975
- The new math of computer programmingCommunications of the ACM, 1975
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- On the calculus of relationsThe Journal of Symbolic Logic, 1941