Assertions and Automation

In the introduction to Hoare Logic we saw that, for programs without loops, it is possible to work top to bottom and generate a large formula that describes the program. If this formula implies the postcondition, then the program is verified against the specification. As programs get more complex we will want to control the structure of these formulas, and to rely on proof automation to prove them.

Making Assertions

So far in Hoare logic we have been relying on the computer to generate a formula after each operation that states what is true about the state of the system at that point. As we have seen, this can lead to quite complex formulas even when there are simpler ways of describing the current state.

For example, if we start with the precondition T, then after we do X := 0, the computer computes the new formula ∃oldX. X = 0 /\ T. This is correct, but it can be replaced by the equivalent and much simpler X = 0.

It often pays to keep the formulas small and informative. Also, as we will see below, when writing programs with while loops it will also be necessary to rewrite the current formula into a more general form in order to prove that the loop works.

We can tell the computer to replace the current formula with a new one by using the command assert (<formula>). For example, this program has the same behaviour as X := 0, but changes the proof to be broken down into two steps.

X := 0
assert (X = 0)
end

Try it here. When you enter assert (X = 0) the computer will ask you to prove that the current formula implies the asserted one. This can be done using auto.

An important point about assert is that the new asserted formula is taken as the complete description of the state of the program at that point. This can be seen in an example:

X := 0
Y := 1
assert (Y = 1)
end

In this program, the assertion Y = 1 is provable, but it forgets that X = 0, so it is not enough to prove a postcondition that X = 0 /\ Y = 1. To fix this, we have to assert everything we want to use later on:

X := 0
Y := 1
assert (X = 0 /\ Y = 1)
end

Try both of these programs in the tool. You will find that doing assert (Y = 1) is allowed, but it will leave the tool in a state where you cannot prove that the postcondition holds at the end of the program.

Using assert can make the proofs we do simpler by keeping the formulas generated by the computer from getting too complex. When we do while loops, it will also be essential to use assert to set up loop invariants.

Proof Automation

The bulk of the proofs involved in verifying programs involve quite a bit of rearrangement of formulas to find the relevant parts (i.e., using first, second, and unpack) and relatively little creativity in how to instantiate universal and existential quantifiers (i.e., using inst and exists). The auto proof rule that we introduced when introducing Hoare logic can do these simple proofs. Specifically it can do any proof that does not involve the rules inst or exists. Notably, it can handle reasoning using any equations that are in the current set of assumptions. For example, it can prove a formula like:

It can even deal with complex uses of ORs:

Every proof in Propsitional Logic can be completed using auto.

However, it cannot handle a formula like:

This is because it does not know what value to instantiate the universal quantifier with. In this case, it is obviously a(), but in general the problem of finding this out is undecidable.

The auto command can still help with proving formulas like this if we provide the correct instantiation of a(). We do this using a new command store which has the following rule:

In words: store takes the formula currently in focus and treats it as a normal assumption. The general use of this is to take a universally quantified assumption, instantiate it to get a quantifier-free version and then add that as an assumption. The auto command can then use this quantifier-free assumption without having to guess the instantiation. For complex proofs we might have to provide several instantiated versions of universally quantified assumptions.

With the help of store, the formula above can be proved using auto. In the prover instance here, enter introduce H, then use H, inst "a()" and store H2 (store needs a name for the new assumption) to add the specific instance to the context. Then auto is able to complete the proof.

The commands auto and store do not increase the power of the proof tool (apart from adding excluded middle). Any proof that uses store could have been completed by repeating the steps that have been stored wherever they are needed, and any proof using auto can be done by hand (assuming excluded middle). So we have not increased the power of our proof system, but we have made it easier to prove formulas, especially ones with deeply nested structure as we see in proofs about programs.