The function `genVerifictionConditions()`

in the class `Compiler`

has to return one value of the type `Formula`

. I’m using two functions for inferring the conditions `toPC()`

and `toVC()`

, it seems like `toVC()`

is using the result from `toPC()`

and in the end I need to combine all VCs to one formula which should be returned. Does it make sense to combine all verification conditions (the result of `toVC()`

) by conjunction and then let the solver check this compound formula?

For example: if my `toVC()`

function has a list of verification conditions `f_1`

, `f_2`

, …, `f_n`

, the result formula, which will be returned to the solver, is should be `f_1 && f_2 && ... && f_n`

?

Furthermore, it was also recommended in the project presentation that we can forgo the two methods `Statement::toPC()`

and `Statement::toVC()`

and declare `Pair Statement::toFormula()`

. What is `Pair Statement`

? Why not `Statement`

?

The general theorem is:

If all formulas in `vc s Q`

and additionally `pc s Q`

are valid, then \{\top\}\,s\,\{Q\}.

Those formulas are valid iff \mathit{pc}\,s\,Q \wedge \left(\bigwedge \mathit{vc}\,s\,Q\right) is valid.

Now, whether `vc s Q`

returns a set of formulas, or a conjunction of formulas, does not really matter. Since we prepared our slides a bit in advance, we used last year’s lecture notes, where `vc`

was defined to return \bigwedge(\mathit{vc}\,s\,Q). Of course, which one you implement, does not matter, since in the end you conjunct them all together anyway.

`Pair Statement::toFormula()`

means that in the class `Statement`

, you have a method called `toFormula()`

which returns a `Pair`

. A `Pair`

is a class you are supposed to define that works like a pair of formulas (or of a formula and a set of formulas).

1 Like

It’s not, at least not immediately. You need both. For simple programs, `vc`

returns the empty set, but that does not mean that such programs are “obviously correct”.

1 Like