Hoare Logic Proof Assistant (Bachelor)

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 Download example outline (PDF, 80 KB)), 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 Bachelor’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. More elaborate strategies are possible, and could be considered as an extension to the project.
Other 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
• Have an impact on how Formal Methods are taught at ETH, and provide a tool that helps students to study Hoare logic
[1] external page http://www.doc.ic.ac.uk/pandora/

Contact