Advertisement

A Mechanized Theory of Program Refinement

  • Boubacar Demba SallEmail author
  • Frédéric Peschanski
  • Emmanuel Chailloux
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

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.

Keywords

Stepwise refinement Program verification Predicative programming Correctness-by-construction Type theory Proof assistant Coq 

Notes

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.

References

  1. 1.
    Alpuim, J., Swierstra, W.: Embedding the refinement calculus in Coq. Sci. Comput. Program. 164, 37–48 (2018)CrossRefGoogle Scholar
  2. 2.
    Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (2012).  https://doi.org/10.1007/978-1-4612-1674-2CrossRefzbMATHGoogle Scholar
  3. 3.
    Backhouse, R., Van Der Woude, J.: Demonic operators and monotype factors. Math. Struct. Comput. Sci. 3(4), 417–433 (1993)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and nondeterministic programs. TCS. 43, 123–147 (1986)MathSciNetCrossRefGoogle Scholar
  5. 5.
    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_6CrossRefGoogle Scholar
  6. 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/BFb0105399CrossRefGoogle Scholar
  7. 7.
    Desharnais, J., Jaoua, A., Mili, F., Boudriga, N., Mili, A.: A relational division operator: the conjugate kernel. TCS 114(2), 247–272 (1993)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Dijkstra, E.: Notes on structured programming. In: Dahl, O.J., Dijkstra, E.W., Hoare, C.A.R. (eds.) Structured Programming. Academic Press, London (1972)zbMATHGoogle Scholar
  9. 9.
    Frappier, M., Mili, A., Desharnais, J.: A relational calculus for program construction by parts. Sci. Comput. Program. 26(1–3), 237–254 (1996)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Hehner, E.C.: Predicative programming Part I. Commun. ACM 27(2), 134–143 (1984)MathSciNetCrossRefGoogle Scholar
  11. 11.
    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_41CrossRefGoogle Scholar
  12. 12.
    Hehner, E.C.: A Practical Theory of Programming. Springer, New York (2012).  https://doi.org/10.1007/978-1-4419-8596-5CrossRefzbMATHGoogle Scholar
  13. 13.
    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_20CrossRefGoogle Scholar
  14. 14.
    Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127–132 (1987)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Knuth, D.E.: Literate programming. Comput. J. 27(2), 97–111 (1984)CrossRefGoogle Scholar
  18. 18.
    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-5CrossRefzbMATHGoogle Scholar
  19. 19.
    Mili, A.: A relational approach to the design of deterministic programs. Acta Informatica 20(4), 315–328 (1983)MathSciNetCrossRefGoogle Scholar
  20. 20.
    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_20CrossRefGoogle Scholar
  21. 21.
    Morgan, C., Robinson, K., Gardiner, P.: On the Refinement Calculus (Formal Approaches to Computing and Information Technology (FACIT)). Springer, London (1994)Google Scholar
  22. 22.
    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_20CrossRefGoogle Scholar
  23. 23.
    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_16CrossRefGoogle Scholar
  24. 24.
    The Coq Development Team: The Coq proof assistant, version 8.8.0, April 2018Google Scholar
  25. 25.
    Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221–227 (1971)CrossRefGoogle Scholar
  26. 26.
    Woodcock, J., Davies, J.: Using Z. Prentice Hall International (1996)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Boubacar Demba Sall
    • 1
    Email author
  • Frédéric Peschanski
    • 1
  • Emmanuel Chailloux
    • 1
  1. 1.Sorbonne Université, CNRS, LIP6ParisFrance

Personalised recommendations