ANSWER TO MOCK QUESTION 2b

PART 1:

G1 =
x : 0 -> 3
x : 5 -> 8

G2 =
x : 0 -> 5
x : 3 -> 5

G2,G1 ⊦
{x=0 ∨ x=5}
x:=x+3
{x=3 ∨ x=5 ∨ x=8}

G1,G2 ⊦
{x=0 ∨ x=3}
x:=5
{x=5 ∨ x=8}

PART 2:

We need to add auxiliary state. The program becomes:

a:=0; b:=0; c:=0;
(
if x=0 then 
||
if x=0 then 
||
if x=0 then 
)

where〈...〉 denotes an atomically-executed code block.

G1 =
x=a --> x=a ∧ a≠0

G2 =
x=b --> x=b ∧ b≠0

G3 =
x=c --> x=c ∧ c≠0

Define I = x=a+b+c. Then the annotated program is:

a:=0; b:=0; c:=0;
{I ∧ a=0 ∧ b=0 ∧ c=0}
c1 || c2 || c3
{I ∧ a∈{0,1} ∧ b∈{0,2} ∧ c∈{0,1} ∧ a+b+c≠0}

That postcondition implies x∈{1,2,3,4} as required.

The individual threads, c1, c2 and c3, are verified like so:

G2∪G3, G1 ⊦
{I ∧ a=0}
if x=0 then
{I ∧ a=0}
〈a:=a+1;x:=x+1〉
{I ∧ a=1}
else
{I ∧ a=0 ∧ b+c≠0}
end if
{I ∧ a∈{0,1} ∧ a+b+c≠0}

G1∪G3, G2 ⊦
{I ∧ b=0}
if x=0 then
{I ∧ b=0}
〈b:=b+2;x:=x+2〉
{I ∧ b=2}
else
{I ∧ b=0 ∧ a+c≠0}
end if
{I ∧ b∈{0,2} ∧ a+b+c≠0}

G1∪G2, G3 ⊦
{I ∧ c=0}
if x=0 then
{I ∧ c=0}
〈c:=c+1;x:=x+1〉
{I ∧ c=1}
else
{I ∧ c=0 ∧ a+b≠0}
end if
{I ∧ c∈{0,1} ∧ a+b+c≠0}