Abstract
Correctness-by-construction (CbC), traditionally based on weakest precondition semantics, and post-hoc verification (PhV) aspire to ensure functional correctness. We argue for a lightweight approach to CbC where lack of formal rigour increases productivity. In order to mitigate the risk of accidentally introducing errors during program construction, we propose to complement lightweight CbC with PhV. We introduce lightweight CbC by example and discuss strength and weaknesses of CbC and PhV and their combination, both conceptually and using a case study.
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
Similar content being viewed by others
Notes
- 1.
Dijkstra-speak for ‘program statement’.
- 2.
We could, of course, apply ever deeper levels of intuition and arrive at the best known algorithms, but we limit our example here to the simplest sorting algorithms.
- 3.
Here, we have written the I in many places to emphasise where it must hold. In most algorithm presentations, it is only mentioned in the line preceding the loop, but the other proof obligations remain (in this case for \(S_3\) to re-establish the invariant).
- 4.
Again, this is barring absurdities such as the length of A changing dynamically, which is precisely the difficulty in parallel programs, in which this may indeed happen.
- 5.
- 6.
There are alternative notational conventions in the literature for total and partial correctness.
- 7.
This is because both \(\textit{False}\implies \textit{True}\) and \(\textit{False}\implies \textit{False}\) evaluate to True,.
- 8.
References
Beck, K.: Extreme Programming Explained: Embrace Change. Addison-Wesley Longman Publishing Co. Inc., Boston (2000)
Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. Softw. IEEE 19(1), 18–25 (2002)
Beckert, B., Hähnle, R.: Reasoning and verification. IEEE Intell. Syst. 29(1), 20–29 (2014)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Havelund, K., Holzmann, G.J., Joshi, R., Bobaru, M. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)
Barnett, M., M. Leino, K.R., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Filliâtre, J.-C., Marché, C.: The why/krakatoa/caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)
Gries, D.: The Science of Programming. Springer, Heidelberg (1987)
Cohen, E.: Programming in the 1990s: An Introduction to the Calculation of Programs. Springer, Heidelberg (1990)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Upper Saddle River (1994)
Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012)
Chapman, R.: Correctness by construction: a manifesto for high integrity software. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software. SCS 2005, vol. 55, pp. 43–46(2006)
Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)
Méry, D., Monahan, R.: Transforming event B models into verified C# implementations. In: First International Workshop on Verification and Program Transformation, VPT 2013, Saint Petersburg, Russia, 12–13 July 2013, pp. 57–73 (2013)
Cheng, Z., Mery, D., Monahan, R.: On two friends for getting correct programs - automatically translating event-B specifications to recursive algorithms in Rodin. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 821–838. Springer, Heidelberg (2016)
Lamprecht, A., Margaria, T., Schaefer, I., Steffen, B.: Synthesis-based variability control: correctness by construction. In: Formal Methods for Components and Objects, 10th International Symposium, pp. 69–88. Revised Selected Papers (2011)
ter Beek, M., Reniers, M., de Vink, E.: Supervisory controller synthesis for product lines using CIF 3. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 856–873. Springer, Heidelberg (2016)
ter Beek, M., Carmona, J., Kleijn, J.: Conditions for compatibility of components - the case of masters and slaves. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 784–805. Springer, Heidelberg (2016)
Cleophas, L., Kourie, D.G., Pieterse, V., Schaefer, I., Watson, B.W.: Correctness-by-construction \(\wedge \) taxonomies \(\Rightarrow \) deep comprehension of algorithm families. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 766–783. Springer, Heidelberg (2016)
ter Beek, M., Hähnle, R., Schaefer, I.: Correctness-by-construction and post-hoc verification - friends or foes? In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 723–729. Springer, Heidelberg (2016)
Lagarias, J.C.: The 3x + 1 problem and its generalizations. IEEE Intell. Syst. 92(1), 3–23 (1985)
Hoare, C.A.R.: Algorithm 64: quicksort. Commun. ACM 4(7), 321 (1961)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Commun. ACM 7(3), 212–232 (2005)
Voelter, M., Benz, S., Dietrich, C., Engelmann, B., Helander, M., Kats, L., Visser, E., Wachsmuth, G.: DSL Engineering - Designing, Implementing and Using Domain-Specific Languages (2013). dslbook.org
Acknowledgments
This work was partially supported by the DFG (German Research Foundation) under grant SCHA1635/2-2, and by the NRF (South African National Research Foundation) under grants 81606 and 93063.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Watson, B.W., Kourie, D.G., Schaefer, I., Cleophas, L. (2016). Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_52
Download citation
DOI: https://doi.org/10.1007/978-3-319-47166-2_52
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47165-5
Online ISBN: 978-3-319-47166-2
eBook Packages: Computer ScienceComputer Science (R0)