VC and PC return

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