Abstract
Hoare-style program verification relies on the construction and discharge of verification conditions (VCs) but offers no support to trace, analyze, and understand the VCs themselves. We describe a systematic extension of the Hoare rules by labels so that the calculus itself can be used to build up explanations of the VCs. The labels are maintained through the different processing steps and rendered as natural language explanations. The generated explanations are based only on an analysis of the labels rather than directly on the logical meaning of the underlying VCs or their proofs. The explanations can be customized to capture different aspects of the VCs; here, we focus on labelings that explain their structure and purpose.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barthe, G., et al.: JACK – a tool for validation of security and behaviour of Java applications. In: Formal Methods for Components and Objects. LNCS, vol. 4709, pp. 152–174. Springer, Heidelberg (2007)
Crocker, D.: Perfect Developer: a tool for object-oriented formal specification and refinement. In: Tool Exhibition Notes, FM 2003, pp. 37–41 (2003)
Denney, E., Fischer, B.: Correctness of source-level safety policies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 894–913. Springer, Heidelberg (2003)
Denney, E., Fischer, B.: Certifiable program generation. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 17–28. Springer, Heidelberg (2005)
Denney, E., Fischer, B.: A program certification assistant based on fully automated theorem provers. In: Proc. Intl. Workshop on User Interfaces for Theorem Provers (UITP 2005), Edinburgh, pp. 98–116 (2005)
Denney, E., Fischer, B.: A generic annotation inference algorithm for the safety certification of automatically generated code. In: GPCE 2006, pp. 121–130. ACM Press, New York (2006)
Denney, E., Trac, S.: A software safety certification tool for automatically generated guidance, navigation and control code. In: IEEE Aerospace Conference Electronic Proceedings, IEEE, Big Sky (2008)
Denney, E., Venkatesan, R.P.: A generic software safety document generator. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 102–116. Springer, Heidelberg (2004)
Fiedler, A.: Natural language proof explanation. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 342–363. Springer, Heidelberg (2005)
Fischer, B., Schumann, J.: AutoBayes: A system for generating data analysis programs from statistical models. J. Functional Programming 13(3), 483–508 (2003)
Fraer, R.: Tracing the origins of verification conditions. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 241–255. Springer, Heidelberg (1996)
Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Science of Computer Programming 55(1–3), 209–226 (2005)
Sutcliffe, G., Denney, E., Fischer, B.: Practical proof checking for program certification. In: Proc. CADE-20 Workshop on Empirically Successful Classical Automated Reasoning (ESCAR 2005), Tallinn (July 2005)
Vallado, D.A.: Fundamentals of Astrodynamics and Applications, 2nd edn. Space Technology Library. Microcosm Press and Kluwer Academic Publishers (2001)
Whittle, J., Schumann, J.: Automating the implementation of Kalman filter algorithms. ACM Trans. Mathematical Software 30(4), 434–453 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Denney, E., Fischer, B. (2008). Explaining Verification Conditions. In: Meseguer, J., Roşu, G. (eds) Algebraic Methodology and Software Technology. AMAST 2008. Lecture Notes in Computer Science, vol 5140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79980-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-79980-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79979-5
Online ISBN: 978-3-540-79980-1
eBook Packages: Computer ScienceComputer Science (R0)