Verification Description

The description states

Shouldn’t it say vc [B] true, as we want to compute the verification conditions, not the precondition?

You want both.
You want to show:

  • The verification condition holds (invariants are invariant and strong enough) and
  • The precondition is satisfied under which the program terminates correctly.

It is more intuitive to think about the use case which usually would be a program beginning with an assume and ending in an assert.

The assert tells the condition generator to prove Q instead of true as it asserts that Q holds at the end of the program.
The assume is there to give certain calling restrictions that impose a precondition on what is believed to be true and not needed to be proved.
Lemma 7.4.13

Additionally, you need the verification condition for the while case as discussed in the lecture.
Under the verification condition, the computed precondition shows the correctness (using Hoare logic) of the program (if it holds).
Combined with soundness and a proof of the vc and pc formula, you obtain semantic correctness of the program.

Thank you for your answer. I think I was confused about the formulation.

So is it correct to say that the formula we need to generate in Compiler::genVerificationConditions is a And-operation over all verification conditions found in our function body, being in essence the ones created via the consequence rule (e. g. whenever an assumption should imply another precondition created by the remainder of the block) and the while verification conditions, therefore including the condition that our program (partially) terminates correctly?

Your wording is rather confusing.

The formula that you need to generate is a conjunction (and-operation) of the precondition and the verification condition of the entire function that you verify, where the verification condition is, like you say, a conjunction of all the verification conditions of individual statements.

1 Like

Is the precondition included because it should be already be universally true in a verifiable function?

Well, kinda. You need to show that all function bodies have pre- and postcondition true. This means showing that \bigwedge \mathit{vc}\ s\ \top \wedge (\top \to \mathit{pc}\ s\ \top), to be formal, where s is the body.

The \top\to implication can be removed since it is redundant. The actual pre/postconditions come in with the _Assume/_Assert ghost statement.

The verification condition for non-empty blocks seems to be missing the union with the verification conditions for all the other statements, as it was written during the lecture.

Indeed, see Verification only one assume meaningful - #4 by johannes

This is a typo. It is corrected and will be changed in the lecture notes. Thanks.

Edit: The corrected version is now online.