Reasoning about Partial Correctness Assertions in Isabelle/HOL

Alfio Ricardo Martini

Abstract


Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented and concurrent programs. The purpose of this work is to provide a detailed and accessible exposition of the several ways the user can conduct, explore and write proofs of correctness of sequential imperative programs with Hoare logic and the ISABELLE proof assistant. With the proof language Isar, it is possible to write structured, readable proofs that are suitable for human understanding and communication.


Keywords


Hoare Logic; program verification; theorem proving

Full Text:

PDF

References


FLOYD, R. W. Assigning meanings to programs. Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, v. 19, 01 1967.

HOARE, C. A. R. An axiomatic basis for computer programming. Commun. ACM, v. 12, n. 10, p. 576–580, 1969.

APT, K. R.; BOER, F. de; OLDEROG, E.-R. Verification of Sequential and Concurrent Programs. 3rd. ed. [S.l.]: Springer Publishing Company, Incorporated, 2009.

ANDREWS, G. R. Concurrent Programming: Principles and Practice. Redwood City, CA, USA: Benjamin-Cummings Publishing Co., Inc., 1991.

NIPKOW, T.; WENZEL, M.; PAULSON, L. C. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin, Heidelberg: Springer-Verlag, 2002.

APPEL, A. W. et al. Program Logics for Certified Compilers. New York, NY, USA: Cambridge University Press, 2014.

BERTOT, Y.; CASTRAN, P. Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. 1st. ed. [S.l.]: Springer Publishing Company, Incorporated, 2010.

FILLI TRE, J.-C. One Logic To Use Them All. In: BONACINA, M. P. (Ed.). CADE 24 - the 24th International Conference on Automated Deduction. Lake Placid, NY, United States: Springer, 2013.

LEINO, R. Dafny: An automatic program verifier for functional correctness. In: 16th International Conference, LPAR-16, Dakar, Senegal. [S.l.]: Springer Berlin Heidelberg, 2010. p. 348–370.

BUBEL, R.; HÄHNLE, R. Key-hoare. In: Deductive Software Verification - The KeY Book - From Theory to Practice. [S.l.: s.n.], 2016. p. 571–589.

WINSKEL, G. The Formal Semantics of Programming Languages - an Introduction. [S.l.]: MIT Press, 1993. I-XVIII, 1-361 p. (Foundation of computing series).

HEIN, J. Discrete Structures, Logic, and Computability. [S.l.]: Jones & Bartlett Learning, 2010.

NIELSON, H. R.; NIELSON, F. Semantics with Applications - a Formal Introduction. [S.l.]: Wiley, 1992. I-XII, 1-240 p. (Wiley professional computing).

BRADLEY, A. R.; MANNA, Z. The Calculus of Computation: Decision Procedures with Applications to Verification. Berlin, Heidelberg: Springer-Verlag, 2007.

LOECKX, J.; SIEBER, K.; STANSIFER, R. D. The Foundations of Program Verification. New York, NY, USA: John Wiley & Sons, Inc., 1984.

GORDON, M. J. C. Programming language theory and its implementation - applicative and imperative paradigms. [S.l.]: Prentice Hall, 1988. (Prentice Hall International series in Computer Science).

NIPKOW, T.; KLEIN, G. Concrete Semantics: With Isabelle/HOL. [S.l.]: Springer Publishing Company, Incorporated, 2014.

PAULSON, L. C. ML for the working programmer (2. ed.). [S.l.]: Cambridge University Press, 1996.

O’SULLIVAN, B.; GOERZEN, J.; STEWART, D. Real world Haskell - code you can believe in. O’Reilly, 2008. Disponível em: http://book.realworldhaskell.org/.

HAFTMANN, F. Haskell-style type classes with Isabelle/Isar. 2019. http://isabelle.in.tum.de/documentation.html.

BLANCHETE, J. User’s Guide to Sledgehammer. 2018. http://isabelle.in.tum.de/documentation.html.

SCHULZ, S.; CRUANES, S.; VUKMIROVIC, P. Faster, higher, stronger: E 2.3. In: Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. [s.n.], 2019. p. 495–507. Disponível em: https://doi.org/10.1007/978-3-030-29436-6_29.

WEIDENBACH, C. et al. Spass version 3.5. In: SCHMIDT, R. A. (Ed.). CADE. [S.l.]: Springer, 2009. (Lecture Notes in Computer Science, v. 5663), p. 140–145.

KOVÁCS, L.; VORONKOV, A. First-order theorem proving and vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044. New York, NY, USA: Springer-Verlag New York, Inc., 2013. (CAV 2013), p. 1–35.

MOURA, L. D.; BJØRNER, N. Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. [S.l.]: Springer-Verlag, 2008. (TACAS’08/ETAPS’08), p. 337–340.

BARRETT, C. et al. CVC4. In: GOPALAKRISHNAN, G.; QADEER, S. (Ed.). Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11). [S.l.]: Springer, 2011. (Lecture Notes in Computer Science, v. 6806), p. 171–177.

PIERCE, B. C. et al. Logical Foundations. [S.l.]: Electronic textbook, 2018. https://softwarefoundations.cis.upenn.edu/. (Software Foundations series, volume 1).

PIERCE, B. C. et al. Programming Language Foundations. [S.l.]: Electronic textbook, 2018. https://softwarefoundations.cis.upenn.edu/. (Software Foundations series, volume 2).

LEINO, K. R. M. This is boogie 2. 2008. Disponível em: https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/.




DOI: https://doi.org/10.22456/2175-2745.98483

Copyright (c) 2020 Alfio Ricardo Martini

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Indexing databases:
        

Acknowledgments: