A Developer-oriented Hoare Logic

Even with current automated reasoning technology, full functional verification requires human interaction to guide the proof: assignments to ghost variables (e.g. [1]) or intermediate assertions (e.g. [17]) need to be provided, and sometimes the prover’s deductions need to be examined in detail (e.g. [1, §7],[13]). Indeed, some authors have argued that the developer’s understanding will be necessary regardless of advances in automation (e.g. [17, §7.2][8, §4.3][2, §1.2]). For effective interaction, the user has to understand the generated verification conditions. While it is possible to relate them back to the source code by suitable highlights and annotations (e.g. [4, 9]), this approach does not cover the verification conditions themselves. For instance, the conditions usually express side-effects in the program by substitutions (e.g. [4, §4.2]), which in a weakest precondition calculus relate only loosely to a developer’s view on the code. We therefore propose to design the Hoare logic and verification environment itself to increase the developer’s understanding of the verification process. Taking lightweight separation [5, 6, 7] as the basis, this paper presents a suite of verification tools developed around that method and their application to case studies. Although the language treated is a C dialect with a finite byteaddressed memory model, even involved algorithms like Schorr-Waite graph traversal lead to natural and readable proof obligations. Since assertions employ classical first-order (or higherorder) logic, existing automated reasoners apply. The tools are developed as a conservative extension of Isabelle/HOL, which ensures their correctness.