Notation for Verification bonus


in the bonus assignment the return type of vc is a formula, not a set of formulas. I assume that the vc on this page, let’s call it vc', is defined as \text{vc' s }Q = \bigwedge \text{vc s }Q. The following should then be valid definitions:

vc break; Q = vc continue; Q = {}

since \bigwedge \emptyset = \text{true}.

In the case of the while rule that would mean that the things that are “and-ed” to the upper vc (which is really a vc') are actually added to that set.

You are correct.

This happened because the presentation of vc has changed this year compared to previous years, where the conjunction was used directly.
For your implementation, you are free to choose whether you want to return a single formula or a collection of formulas.

vc is now notated as set in the project description to match the lecture notes.