Explaining Verification Conditions

The Hoare approach to 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 explanations can easily be customized and can capture different aspects of the VCs; here, we focus on labelings that explain their structure and purpose. The approach is fully declarative and 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.

• Type: Conference
• Year: 2008
• Where: AMAST
• Authors: Ewen Denney, Bernd Fischer 0002
• Keywords: AMAST 2008, Hoare Approach, Labels, Natural Language Explanations, Software Engineering