Abstract
The correctness by construction methodology advocated by this book starts off with a predicate-based specification of the problem at hand, and then incrementally refines that specification to code. However, to be able to do this, several preliminary notational and theoretical matters have to be in place.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
i.e. a method that returns a Boolean value.
- 2.
Note that by this definition S is stronger than itself, since \((S\Rightarrow S)\) is a tautology—i.e. \((S\Rightarrow S) \equiv \mathrm{true}\).
- 3.
In some texts, P{S}Q is interpreted as a statement of partial correctness, by which is meant the assertion that if P is true and S executes then Q will be true, ifS terminates.
- 4.
There are at least four different approaches to defining the semantics of S: operationally; translationally; denotationally; and axiomatically. Details are beyond the scope of this text. However, it may be of interest to note that the precondition approach is generally classified as an axiomatic approach to defining semantics, and we usually speak of the “precondition semantics” in this context.
- 5.
Although program constructs are commonly referred to as statements, Dijkstra preferred the term command. For this reason, the term shall be used consistently throughout this text.
- 6.
In fact, the ADA select command is inspired by the GCL command, as is the choice operation in CSP (and subsequent CSP variants such as FSP as a specification language and Occam as an implementation language).
- 7.
As a matter of convention, an integer expression rather than a real-valued expression is used, and normally the variant is scaled so that it is bounded from below by 0.
References
D.G. Kourie, An approach to defining abstractions, refinements and enrichments. Quæst. Inf. 6(4), 174–178 (1989)
B. Meyer, Touch of Class: Learning to Program Well with Objects and Contracts (Springer-Verlag, Berlin, Heidelberg, 2009)
C. Morgan, Programming from specifications (1998), http://web2.comlab.ox.ac.uk/oucl/publications/books/PfS/
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kourie, D.G., Watson, B.W. (2012). Background. In: The Correctness-by-Construction Approach to Programming. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27919-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-27919-5_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27918-8
Online ISBN: 978-3-642-27919-5
eBook Packages: Computer ScienceComputer Science (R0)