Abstract
There are many debates amongst software engineers about the extent to which one should engage in so-called upfront design. But the focus of the debate relates mostly to programming-in-the-large: how to approach the problem of designing a large system of interacting objects or components.
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.
How one finds an invariant for a sequence of steps cannot be prescribed. It is very much dependent on the problem to be solved. It is an art that comes with practice.
- 2.
Actually, we could make the invariant even more precise, namely \(\mathrm{number(white)} + 2 = \mathrm{number(black)}\). However, this increased precision does not help us any further in solving the problem.
- 3.
As will be seen later, this is an example of a so-called variant—a function that strictly decreases towards a fixed minimum value. It guarantees that the problem can be solved in a finite number of steps.
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). Introduction. In: The Correctness-by-Construction Approach to Programming. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27919-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-27919-5_1
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)