Explaining Verification Conditions
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
- PDF / 449,676 Bytes
- 15 Pages / 430 x 660 pts Page_size
- 36 Downloads / 218 Views
2
USRA/RIACS, NASA Ames Research Center, Moffett Field, CA 94035, USA [email protected] DSSE Group, School of Electronics and Computer Science, University of Southampton, UK [email protected]
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.
1 Introduction Program verification is easy when automated tools do all the work: a verification condition generator (VCG) takes a program that is “marked-up” with logical annotations (i.e., pre-/post-conditions and invariants) and produces a number of verification conditions (VCs) that are simplified, completed by a domain theory, and finally discharged by an automated theorem prover (ATP). In practice, however, many things can, and typically do, go wrong: the program may be incorrect or unsafe, the annotations may be incorrect or incomplete, the simplifier may be too weak, the domain theory may be incomplete, or the ATP may run out of resources. In each of these cases, users are typically confronted only with failed VCs (i.e., the failure to prove them automatically) but receive no additional information about the causes of the failure. They must thus analyze the VCs, interpret their constituent parts, and relate them through the applied Hoare rules and simplifications to the corresponding source code fragments. Even if all VCs can be proven automatically, there is often still a need to understand their intent, for example if the formal verification is being used to support a code review. Unfortunately, VCs are a detailed, low-level representation of both the underlying information and the process used to derive it, so understanding them is often difficult. Here we describe an technique that helps users to trace and understand VCs. Our idea is to systematically extend the Hoare rules by “semantic mark-up” so that we can use the calculus itself to build up explanations of the VCs. This mark-up takes the form of structured labels that are attached to the meta-variables used in the Hoare rules (or to the annotations in the program), so that the VCG produces labeled versions of the VCs. The labels are maintained through the different processing steps, and are then extracted from the final VCs and rendered as natural language explanations. J. Meseguer and G. Ros¸u (Eds.): AMAST 2008, LNCS 5140, pp. 145–159, 2008. c Springer-Verlag Berlin Heidelberg 2008
146
E. Denney and B. Fis
Data Loading...
