Developing a Hoare Logic Proof Assistant
Hoare Logic Proof Assistant (Master)
Background
Hoare logics (which are axiomatic semantics) are a family of formal systems for reasoning about properties of programs; they are used to prove correctness and termination of programs. Hoare logic is a derivation system, and as such, a proof in Hoare logic is represented as a proof tree. However, when proving program properties on paper – as is common when learning/teaching Hoare logic – such proofs are usually represented as proof outlines (see the example outline on page 3), which is more convenient to work with.
Working with proof outlines is still not trivial, though, because choosing the (or a) correct rule to apply is sometimes not obvious, especially for students not yet familiar with Hoare logic. Moreover, many students struggle with applying the chosen rule in a rigorous way, i.e. in a way that strictly follows the rules of the system, because they already apply simplifications which are often intuitively correct, but need to be justified by additional rule applications.
These challenges (and others) can be addressed by using a tool (e.g. a graphical editor such as [1]) that supports constructing and modifying proof outlines. More importantly, experiments in closely related areas indicate that getting immediate feedback – as provided by tools – during the construction of a proof outline (e.g. while working on homework assignments) could significantly improve the learning success of students; especially when compared to the traditional exercise session cycle, where students get feedback with a delay of a week or even more.
Project
The goal of this Master’s project is to create a visual Hoare logic proof assistant for teaching purposes, e.g. in the course Formal Methods and Functional Programming offered at ETH. The focus of the tool should therefore be on usability and feedback rather than on power and expressiveness. The tool could be implemented as a desktop tool (most likely in Scala), but it might also be possible to implement it as a web application.
The project should address the following tasks:
• Offer two modes for constructing proof outlines: (A) Select an assertion and a statement, e.g. if-then-else, and press a button to apply a rule, e.g. the if-rule. If applicable, the tool will apply the rule and fill in the still missing assertions, if not, it will provide a helpful error message. (B) The user provides all assertions and then uses the tool to check if all assertions correspond to correct rule applications.
• Represent partial proof outlines in a way that supports both forward and backward reasoning
• Support partial and total correctness (total correctness includes proving termination of loops)
• Support non-linear undoing, e.g. undo only the work done in the if-branch, although it was done before working on the else-branch
• Support pretty-printing of proof outlines (e.g. via LaTeX)
• Develop and implement (at least one) strategy for handling the rule of consequence, i.e. for proving the correctness of entailments (implications)
Regarding the rule of consequence, one strategy would be to not check anything and to simply trust the user that the resulting entailments, e.g. x > 0 ∧ y < 0 ⊨ x * y < 0, are actually true. Ideally, the editor allows the user to add textual comments to informally argue why the entailment is true.
A more elaborate strategy would be to encode the entailment in a language that is understood by an automated verifier/prover, which would then try to prove the entailment (without further user interaction). This strategy, however, gives rise to additional research questions:
• Would it be useful to extend the proof outline editor such that the user can perform a case split to justify an application of the rule of consequence?
• How to define functions, e.g., the greatest common divisor or the Fibonacci function?
• How to handle proofs by induction?
A third strategy would be to integrate a natural deduction proof assistant into the Hoare logic proof assistant, which could be used to justify applications of the rule of consequence.
Possible extensions of this project include supporting additional language features such as method calls or non-determinism, and additional proof features such as the frame rule, disjunctions or auxiliary logical variables.
Opportunities
• Become familiar with formal reasoning frameworks such as Hoare logic, and how they can be implemented in tools
• Develop a visual editor using Scala (a modern programming language with an advanced type system that combines object-oriented and functional concepts) or state-of-the-art web techniques
• Gain experience with automated provers/verification tools, and understand how to use them to prove non-trivial program properties
• Have an impact on how Formal Methods are taught at ETH, and provide a tool that helps students to study Hoare logic