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 )

**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:

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)