Hey all,

I’ve just discovered a cool tool that can be used to do Hoare-logic proofs. See https://proof-tree-builder.github.io/

The user interface is a bit weird, but it’s not that hard to work with it. You can start by clicking on `Help`

and doing one of the examples. Ignore everything about sequent calculus. For example, here is my solution for the “counting up to 3” example:

Note that there are a few minor differences between our `C0`

and their language. Notably,

- instead of blocks, there are sequents. So instead of
`{a b ... s}`

we have`a;; b;; .. ;; s`

. - There is no empty block / statement. Simulate it with something like
`x = x`

, which simulates the empty statement (and in particular has the same proof rule) - There is no
`abort()`

. - The rule names are a bit different (
`Loop`

vs`While`

etc) - The syntax differs a bit, like that we write
`while .. do`

and`:=`

for assignments.

Note that when applying the Consequence rule, you get the logical proof goals (which you have to manually prove when doing this on paper). Now, this tool also aims to teach you a certain formal system for formally denoting proofs. Since that’s out of scope for Programming 2, they also have a handy rule called “Z3” which applies the Z3 automatic theorem prover to those logical goals, in a way similar to what we do in the verification part of the compiler projects.

In practice, this means that the Consequence rule generates goals like this:

This means that you have to prove that ((x < 0) \vee (x = 0)) \Rightarrow x \leq 0. The \vdash symbol basically means implication (note that you can also have the \rightarrow implication, the difference does not really matter). Now, you should try to come up with a formal proof for these statements, on paper, to practice your proof writing skills. Luckily, the computer is able to check these kinds of statements. Just apply the “Z3” rule to check whether the given implication is true or not. If it is true, the bar becomes green, otherwise it turns red. Since this formula is true, it looks like this:

Otherwise, you get a counterexample:

I’m sorry that I discovered this only now, given that the re-exam is in < two days. But practicing for an hour with this tool will likely significantly improve your Hoare proof rule abilities. Also, for best results practice with the mode switch on the top right set to “Learn” (like this):

Have fun, and good luck on Friday!