Problem 1:

1. AX(b2) holds exactly on each state in {s8}

2. EX(b2) holds exactly on each state in {s1, s8, s9}

3. EG(!b2) holds exactly on each state in {s0, s1, s6, s10, s11}

4. AG(b1 => AF(b2)) holds on all states.


Problem 2:

1. one state, both initial and accepting, with a self loop (!@p3 v !@q3)

2. (@p0, @q0) -> (@p1, @q0) -> (@p1, @q1) -> (@p1, @q2) -> (@p1, @q3) -> (@p2, @q3) -> (@p3, @q3)

3. Two states: s1 and s2 with s1 initial and accepting.

s1 -> s1 on !@p1
s1 -> s2 on @p1
s2 -> s2 on true
s2 -> s1 on $p3

4. (@p0, @q0) -> (@p1, @q0) -> (@p1, @q1) -> (@p2, @q1) -> (@p3, @q1) -> (@p0, @q1) -> (@p1, @q1) then q ignored forever.

Problem 3:

1. Explain why x2=2 and x1=1 makes the formula sat.

2.

   v0
0/  \1
v1   v1
| \1/ |0
|0 \  |
| /1\ |
v2   v2
| \0/ |1
|1 /  |
| /0\ |
0     1

Problem 4:

1. Postcondition: y = 2^n

2. Partial correctness:

A good invariant: (y=2^i and i <= n)

* Q => Inv with Q=(i=0 and y=1 and 0<=n) and Inv=(y=2^i and i <= n)

Assume i=0, y=1, 0<=n as given by Q

y=2^i is true because y=1 and i=0 by assumption

i <= n because i=0 and 0<=n by assumption

* {Inv and B} y:= 2*y; i:=i+1 {Inv}

assume y=2^i and i<=n and i<n as given by Inv and B

show wp(y:= 2*y; i:=i+1, y=2^i and i<=n) holds.

  wp(y:= 2*y; i:=i+1, y=2^i and i<=n)
= wp(y:= 2*y, wp(i:=i+1, y=2^i and i<=n))
= wp(y:= 2*y, y=2^(i+1) and i+1<=n)
= (2*y=2^(i+1) and i+1<=n)

2*y=2^(i+1) is equivalent to y=2^i which is true by assumption
i+1<=n is equivalent to i < n which is true by assumption

so wp(y:= 2*y; i:=i+1, y=2^i and i<=n) holds and the tripple
{Inv and B} y:= 2*y; i:=i+1 {Inv} is valid.

* {Inv and !B} => R:

We assume y=2^i and i<=n and !(i<n) as given by Inv and !B.

We show R, i.e., y=2^n, holds.

i<=n and !(i>n) both hold by assumption and hence i=n.

Since y=2^i and i=n hold, then y=2^n also holds.


3. Total correctness:

Partial correctness was shown above with the loop invariant

Inv = (y=2^i and i<= n).

Use v=n-i as variant.

Show variant is positive:

{Inv and B} => v>0

Assume y=2^i, i<=n, i<n as given by Inv and B.

Show v>0:

  v>0 
= n-i>0
= n>i
= true by assumption i<n

Show variant decreases at each iteration of the loop:

{Inv and v=v0} stmt {v < v0}

Assume y= 2^i, i<=n, i<n, n-i=v0 as given by Inv, v=v0 and the
definition of v.

show wp(y:=2^i; i:= i+1, n-i < v0) holds.

  wp(y:=2^i; i:= i+1, n-i < v0)
= wp(y:=2^i, wp(i:=i+1, n-i < v0))
= wp(y:=2^i, n-i-1 < v0)
= n-i-1 < v0
= v0-1<v0 (by assumption n-i = v0)
= -1 < 0
= true (arithmetic)

Hence wp(y:=2^i; i:= i+1, n-i < v0) holds and the tripple
{Inv and v=v0} stmt {v < v0} is valid.