Hello,

in exercise 13.11 we are asked to verify a program, which I call `s`

here, against a given specification `(P, Q)`

. So I computed `pc s Q = true`

and `vc s Q = {}`

and applied judgment 7.4 from section 7.4.3 to derive the Hoare triple `{P} s {Q}`

. But when I opened the solution there was a huge proof tree that is completely unreadable. (It even has “…” )

The `pc`

, `vc`

approach seems to go “forwards” while the judgment approach goes “backwards”. Assuming that we get the defining equations of `pc`

and `vc`

in the exam is it allowed to use those instead of the inference rules? Not only are they easier, but from what I understand they also yield weaker conditions than we might come up with (except maybe for loops).

The `pc`

(and `vc`

for while side conditions) function is used to compute a precondition that is strong enough to prove correctness.

At the same time, we defined `pc`

to be as weak as possible (the weakest for everything except while).

Due to lemma Theorem 7.4.11, you could also prove that the given precondition `P`

implies the (nearly weakest) precondition `pc s Q`

(using consequence here) and that `vc s Q`

holds.

The tree is the proof using the hoare calculus.

As we have seen in the lecture, both proofs are basically the same.

Every computation step in `pc`

, `vc`

is a rule application/choice in the hoare proof tree.

I don’t quite understand what you mean by forward and backward.

Both approaches (hoare and `pc`

) are backward in the sense that you go from the back of the program to the front.

You want to derive a precondition from a given postcondition.

For Hoare, this is not entirely true as you can freely choose what to do.

But, for instance, the assign rule implies a backward reasoning style.

(Note: There are post condition computation formulas and there are also ways to define alternative equivalent Hoare rules for assign)

If you do the proof correctly including the connecting steps and the exercise does not explicitly require a Hoare inference proof tree, you can also do a proof using `pc`

and `vc`

.

With the lemmas you have seen you know that this proof is also completely and formally correct.

The only difference is that it hides your choice behind a computation and moves the implication reasoning from its local place to a formula in the end.

It yields (except for loops) the weakest conditions.

But for correctness alone (or satisfaction of specification) any sufficiently weak pre-/intermediate-condition is good enough. With a too strong condition, you will directly notice the place in the tree as it fails there.

The advantage of giving away the choice might be a good argument. But you should also understand the reasoning behind the functions and their connection to the trees.