PSA: Defining equations for pc and vc

This is meant to be a collection of all rules for pc and vc, most of which can be found in the lecture notes, but certainly not all.

I don’t make any promises for correctness and I don’t include much about semantic rules that have to be followed. This is meant as an easy to read reference which has everything in one place. (Also this is part of my revision for the exam, so maybe I learn more writing it, than you will reading it :upside_down_face:)


Notation
Throughout s (with or without subscript) refers to a statement, e to an expression and Q to a formula. I leave out all the [| |]-brackets from the lecture because you only ever have to write them during the exam anyway. (On paper you use spacing and in Java you are forced to separate the arguments by the syntax)

As in the reference grammar a ? means that something is optional.

I use the \wedge-ed version of vc which you obtain as follows from the lecture’s function which I call vc' for clarity:

vc s Q = /\ vc' s Q

where of course \bigwedge\emptyset = \text{true}. This is much more comfortable to implement btw.

Precedence of operators is ! && || =>.


Declarations & Assignments
Here x is an identifier, t is a type and Q[e/x] is the formula Q with all instances of x replaced by the expression e.

pc x = e; Q = Q[e/x]
vc x = e; Q = true
pc t x; Q = Q
vc t x; Q = true

The statement t x = e can be realized as t x; x = e;.


Blocks

pc {} Q = Q
vc {} Q = true
pc {s_1, ..., s_n} Q = pc s_1 pc {s_2, ..., s_n} Q
vc {s_1, ..., s_n} Q = (vc s_1 pc {s_2, ..., s_n} Q)
                    && vc {s_2, ..., s_n} Q

Note that n = 1 is allowed.


Assume & Assert

pc _Assume(e); Q = e => Q
vc _Assume(e); Q = true
pc _Assert(e); Q = e && Q
vc _Assert(e); Q = true

Return

pc return e?; Q = true
vc return e?; Q = true

Branching

pc if (e) s Q = (e && pc s Q) || (!e && Q)
vc if (e) s Q = pc s Q
pc if (e) s_1 else s_2 Q = (e && pc s_1 Q) || !e && pc s_2 Q    // OR
vc if (e) s_1 else s_2 Q = (vc s_1 Q) && vc s_1 Q               // AND

Loops
These are the rules in case no termination expression is given:

pc while(e)_Invariant(i) s Q = i
vc while(e)_Invariant(i) s Q = (vc s i)
                            && (e && i => pc s i)
                            && | i => Q         , if s contains a non-nested break statement
                               | !e && i => Q   , else
pc break; Q = i
vc break; Q = true
pc continue; Q = i
vc continue; Q = true

and this is the “general” case:

pc while(e)_Invariant(i)_Term(t; k) s Q = i && (0 <= t)
vc while(e)_Invariant(i)_Term(t; k) s Q = (vc s i && (0 <= t <= k))
                                       && (e && i && (0 <= t <= k + 1) => (pc s i && (0 <= t <= k)))
                                       && | i => Q         , if s contains a non-nested break statement
                                          | !e && i => Q   , else
pc break; Q = i
vc break; Q = true
pc continue; Q = i && (0 <= t <= k)
vc continue; Q = true

Currying ( \wedge b \dashv b \Rightarrow)
Because I already saw it in a verification related question and it might not be immediately obvious:

\forall abc. (a \wedge b) \Rightarrow c \iff a \Rightarrow (b \Rightarrow c)

where \iff has the lowest precedence and the parenthesis may all be dropped due to precedence of conjunction and the right associativity of implication. (You do not lose any information doing so, but the general pattern for this kind of rule is easier to spot if they are there. Not everyone agrees though)

3 Likes

here you probably want a vc not pc.

Also interesting: (in general; not for exam preparation)

For an alternative presentation (compared to our lecture).

It seems that this rule is not valid:

A counter example is the absolute function, whose body is:

{
  if (x<0) 
      x = 0 - x; 
  _Assert(x >= 0); 
  return x;
}

According to the rule, you mentioned, the pc [abs_func] true = ((x < 0) && (0 - x >= 0)) && true which does not hold for x>=0.

An alternative might be:
pc if (e) s Q = e && pc s Q || !e

1 Like

That is also not quite enough.

The correct rule would desugar the conditional to

if(e) 
  s1
else {}
pc (if e s) Q = (e && pc s1 Q) || (!e && Q)

You need to show that Q holds if the conditional consequence branch is not taken.

2 Likes

Yes, I was too quick on that. And incidentally my code is wrong :slight_smile: I will edit it after 10pm.