Abstract
We present a mechanized theory of program refinement that allows for the stepwise development of imperative programs in the Coq proof assistant. We formalize a design language with support for gradual refinement and a calculus which enforces correctness-by-construction. A notion of program design captures the hierarchy of refinement steps resulting from a development. The underlying theory follows the predicative programming paradigm where programs and specifications are both easily expressed as predicates, which fit naturally in the dependent type theory of the proof assistant.
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.
Calculus of weakest preconditions.
- 2.
- 3.
References
Alpuim, J., Swierstra, W.: Embedding the refinement calculus in Coq. Sci. Comput. Program. 164, 37–48 (2018)
Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (2012). https://doi.org/10.1007/978-1-4612-1674-2
Backhouse, R., Van Der Woude, J.: Demonic operators and monotype factors. Math. Struct. Comput. Sci. 3(4), 417–433 (1993)
Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and nondeterministic programs. TCS. 43, 123–147 (1986)
Boulmé, S.: Intuitionistic refinement calculus. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 54–69. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73228-0_6
Butler, M., Långbacka, T.: Program derivation using the refinement calculator. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 93–108. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0105399
Desharnais, J., Jaoua, A., Mili, F., Boudriga, N., Mili, A.: A relational division operator: the conjugate kernel. TCS 114(2), 247–272 (1993)
Dijkstra, E.: Notes on structured programming. In: Dahl, O.J., Dijkstra, E.W., Hoare, C.A.R. (eds.) Structured Programming. Academic Press, London (1972)
Frappier, M., Mili, A., Desharnais, J.: A relational calculus for program construction by parts. Sci. Comput. Program. 26(1–3), 237–254 (1996)
Hehner, E.C.: Predicative programming Part I. Commun. ACM 27(2), 134–143 (1984)
Hehner, E.C.: Specified blocks. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 384–391. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69149-5_41
Hehner, E.C.: A Practical Theory of Programming. Springer, New York (2012). https://doi.org/10.1007/978-1-4419-8596-5
Hoare, C.A.R.: Proof of correctness of data representations. In: Gries, D. (ed.) Programming Methodology, pp. 269–281. Springer, New York (1978). https://doi.org/10.1007/978-1-4612-6315-9_20
Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127–132 (1987)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)
Josephs, M.B.: An introduction to the theory of specification and refinement. In: IBM research Report RC 12993. IBM Thomas J. Watson Research Division (1987)
Knuth, D.E.: Literate programming. Comput. J. 27(2), 97–111 (1984)
Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27919-5
Mili, A.: A relational approach to the design of deterministic programs. Acta Informatica 20(4), 315–328 (1983)
Morgan, C.: The refinement calculus, and literate development. In: Möller, B., Partsch, H., Schuman, S. (eds.) Formal Program Development. LNCS, vol. 755, pp. 161–182. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57499-9_20
Morgan, C., Robinson, K., Gardiner, P.: On the Refinement Calculus (Formal Approaches to Computing and Information Technology (FACIT)). Springer, London (1994)
Sekerinski, E.: A calculus for predicative programming. In: Bird, R.S., Morgan, C.C., Woodcock, J.C.P. (eds.) MPC 1992. LNCS, vol. 669, pp. 302–322. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56625-2_20
Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 237–252. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74464-1_16
The Coq Development Team: The Coq proof assistant, version 8.8.0, April 2018
Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221–227 (1971)
Woodcock, J., Davies, J.: Using Z. Prentice Hall International (1996)
Acknowledgment
We are very grateful to Sylvain Boulmé and Pierre-Évariste Dagand for all the insightful discussions we had about this work. We also thank the anonymous referees for their useful suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Sall, B.D., Peschanski, F., Chailloux, E. (2019). A Mechanized Theory of Program Refinement. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)