Abstract
Calculational proofs—proofs by stepwise formula manipulation—are praised for their rigor, readability, and elegance. It seems desirable to reuse this style, often employed on paper, in the context of mechanized reasoning, and in particular, program verification.
This work leverages the power of SMT solvers to machine-check calculational proofs at the level of detail they are usually written by hand. It builds the support for calculations into the programming language and auto-active program verifier Dafny. The paper demonstrates that calculations integrate smoothly with other language constructs, producing concise and readable proofs in a wide range of problem domains: from mathematical theorems to correctness of imperative programs. The examples show that calculational proofs in Dafny compare favorably, in terms of readability and conciseness, with arguments written in other styles and proof languages.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011)
Back, R., Grundy, J., von Wright, J.: Structured calculational proof. Formal Aspects of Computing 9(5-6), 469–483 (1997)
Back, R.-J.: Structured derivations: a unified proof style for teaching mathematics. Formal Aspects of Computing 22(5), 629–661 (2010)
Backhouse, R.: Special issue on the calculational method. Information Processing Letters 53(3), 121–172 (1995)
Backhouse, R., Verhoeven, R., Weber, O.: Math\(\int\)pad: A system for on-line preparation of mathematical documents. Software — Concepts and Tools 18(2), 80 (1997)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Bauer, G., Wenzel, M.T.: Calculational reasoning revisited: an Isabelle/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75–90. Springer, Heidelberg (2001)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development — Coq’Art: The Calculus of Inductive Constructions. Springer (2004)
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: BOOGIE 2011: Workshop on Intermediate Verification Languages, pp. 53–64 (2011)
Böhme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 107–121. Springer, Heidelberg (2010)
Chisholm, P.: Calculation by computer. In: Third International Workshop on Software Engineering and its Applications, Toulouse, France, pp. 713–728 (December 1990)
Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 392–406. Springer, Heidelberg (2013)
Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69–84. Springer, Heidelberg (2008)
Dijkstra, E.W.: EWD1300: The notational conventions I adopted, and why. Formal Asp. Comput. 14(2), 99–107 (2002)
Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Texts and monographs in computer science. Springer (1990)
Grundy, J.: Transformational hierarchical reasoning. Comput. J. 39(4), 291–302 (1996)
Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (2008)
Jacobs, B., Smans, J., Piessens, F.: VeriFast: Imperative programs as proofs. In: VS-Tools workshop at VSTTE 2010 (2010)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)
Koenig, J., Leino, K.R.M.: Getting started with Dafny: A guide. In: Software Safety and Security: Tools for Analysis and Verification, pp. 152–181. IOS Press (2012)
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)
Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315–331. Springer, Heidelberg (2012)
Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Ball, T., Zuck, L., Shankar, N. (eds.) Usable Verification Workshop (2010), http://fm.csl.sri.com/UV10/
Manolios, P., Moore, J.S.: On the desirability of mechanizing calculational proofs. Inf. Process. Lett. 77(2-4), 173–179 (2001)
Nipkow, T.: Programming and Proving in Isabelle/HOL (2012), http://isabelle.informatik.tu-muenchen.de/
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Robinson, P.J., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. J. Log. Comput. 3(1), 47–61 (1993)
Rudnicki, P.: An overview of the MIZAR project. In: University of Technology, Bastad, pp. 311–332 (1992)
Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: An automated prover for properties of recursive data structures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407–421. Springer, Heidelberg (2012)
van de Snepscheut, J.L.A.: Proxac: an editor for program transformation. Technical Report CS-TR-93-33, Caltech (1993)
van Gasteren, A.J.M., Bijlsma, A.: An extension of the program derivation format. In: PROCOMET 1998, pp. 167–185. IFIP Conference Proceedings (1998)
Verhoeven, R., Backhouse, R.: Interfacing program construction and verification. In: World Congress on Formal Methods, pp. 1128–1146 (1999)
von Wright, J.: Extending window inference. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 17–32. Springer, Heidelberg (1998)
Wenzel, M.: Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leino, K.R.M., Polikarpova, N. (2014). Verified Calculations. In: Cohen, E., Rybalchenko, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2013. Lecture Notes in Computer Science, vol 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-54108-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54107-0
Online ISBN: 978-3-642-54108-7
eBook Packages: Computer ScienceComputer Science (R0)