var x: int· x:= 2. y:= x+z
= ∃x, xʹ: int· xʹ=2 ∧ yʹ = 2+z ∧ zʹ=z
= yʹ = 2+z ∧ zʹ=z var x: int· y:= x
= ∃x, xʹ: int· xʹ=x ∧ yʹ=x ∧ zʹ=z
= zʹ=z
var x: int· y:= x–x
= yʹ=0 ∧ zʹ=z
one-point for xʹ and idempotent for x
Variable Declaration
var x: T· P declare local state variable x with type T and scope P = ∃x,xʹ:T·P
one-point for x and xʹ
1/77
var x: T· P
= ∃x: undefined· ∃xʹ: T, undefined· P
varx:T:=e· P
= ∃x: e· ∃xʹ: T· P
Variable Declaration
2/77
Variable Suspension
Suppose the state consists of variables w , x , y , and z .
framew,x·P within P, y and z areconstants(no yʹ and zʹ)
= P ∧ yʹ=y ∧ zʹ=z
x:=e = framex·xʹ=e
ok = frame·⊤
s:=ΣL ⇐ frames· varn:nat· sʹ=ΣL
sʹ=ΣL ⇐
3/77
A i := e = Aʹi=e ∧ (∀j· j⧧i ⇒ Aʹj=Aj) ∧ xʹ=x ∧ yʹ=y ∧ …
i:= 2. Ai:= 4. Ai=A2 i:= 2. 4=A2
4=A2
✗ Substitution Law ✔ Substitution Law ✗ Substitution Law
=
=
= =⊥✗
A2:= 2.
= A2:= 2.
= 2=2
= ⊤✗
A(A2):= 3. A2=2
A2=2
✗ Substitution Law ✗ Substitution Law
A2:= 3. A2:= 3. A2:= 3. 4=3
Array
4/77
A i := e = Aʹi=e ∧ (∀j· j⧧i ⇒ Aʹj=Aj) ∧ xʹ=x ∧ yʹ=y ∧ … = Aʹ=i→e|A ∧ xʹ=x ∧ yʹ=y ∧…
= A:=i→e|A
A2:= 3. i:= 2. Ai:= 4. Ai=A2
=
=
=
= =⊤
Substitution Law Substitution Law = is reflexive Substitution Law
A:= 2→3 | A. i:= 2. A:= i→4 | A. Ai =A2 A:= 2→3 | A. i:= 2. (i→4 | A)i = (i→4 | A)2 A:= 2→3 | A. (2→4 | A)2 = (2→4 | A)2
A:= 2→3 | A. ⊤
Array
5/77
A i := e = Aʹi=e ∧ (∀j· j⧧i ⇒ Aʹj=Aj) ∧ xʹ=x ∧ yʹ=y ∧ … = Aʹ=i→e|A ∧ xʹ=x ∧ yʹ=y ∧…
= A:=i→e|A
A2:= 2. A(A2):= 3. A2=2
=
=
=
=
= =⊥
Substitution Law Substitution Law
A:= 2→2 | A. A:= A2→3 | A. A2=2 A:= 2→2 | A. (A2→3 | A)2 = 2 ((2→2 | A)2→3 | 2→2 | A) 2 = 2 (2→3 | 2→2 | A) 2 = 2
3 =2
Array
6/77
remember
Ai:= e becomes A:= i→e | A Aij:= e becomes A:= (i;j)→e | A
Array
7/77
person = “name” → text | “age” → nat
var p: person
p:= “name” → “Josh” | “age” → 17 p “age”:= 18
p:= “age” → 18 | p
Record
8/77
W ⇐ whilebdoPod means
W ⇐ ifbthenP. Welseokfi to prove
sʹ = s + Σ L [n;..#L] ∧ tʹ = t + #L – n ⇐
while n⧧#L do s:= s + Ln. n:= n+1. t:= t+1 od
prove instead
sʹ = s + Σ L [n;..#L] if n⧧#L then
∧ tʹ = t + #L – n ⇐
s:= s + Ln. n:= n+1. t:= t+1.
sʹ = s + Σ L [n;..#L] ∧ tʹ = t + #L – n
else ok fi
While Loop
9/77
means
L ⇐ do
A.
exit when b.
C
od
L ⇐ A. ifbthenokelseC. Lfi
Exit Loop
10/77
means
P ⇐ do
A.
do
od.
E
od
P ⇐ A. Q
Q ⇐ B. ifcthenok elseD. Qfi
B.
exit 2 when c. D
Deep Exit
11/77
means
P ⇐ do
A.
exit 1 when b. C.
do
D.
exit 2 when e. F.
exit 1 when g. H
od.
I
od
Deep Exit
P ⇐ A. ifbthenokelseC.Qfi
Q ⇐ D. ifethenokelseF. ifgthenI. PelseH. Qfifi
12/77
P =
Q =
R =
P ⇐
if x: A (0,..n) (0,..m) then x = A iʹ jʹ else iʹ=n ∧ jʹ=m fi if x: A (i,..n) (0,..m) then x = A iʹ jʹ else iʹ=n ∧ jʹ=m fi
if x: A i (j,..m), A (i+1,..n) (0,..m) then x = A iʹ jʹ else iʹ=n ∧ jʹ=m fi i:= 0. i≤n ⇒ Q
Two-Dimensional Search
i≤n⇒Q ⇐ ifi=nthenj:=melsei
= (xʹ=2)/6 + (xʹ=3)/6 + (xʹ=5)/6 + (xʹ=6)/2. x>3
= Σxʹʹ· ((xʹʹ=2)/6 + (xʹʹ=3)/6 + (xʹʹ=5)/6 + (xʹʹ=6)/2) × (xʹʹ>3)
= 1/6× (2>3) + 1/6× (3>3) + 1/6× (5>3) + 1/2× (6>3)
= 2/3
Average
63/77
Random Number Generator
rand n has value r with probability (r: 0,..n) / n
x=x therefore rand n = rand n ?
x+x = 2×x therefore rand n + rand n = 2 × rand n ?
Replace rand n with r: int with distribution (r: 0,..n) / n Replace rand n with r: 0,..n with distribution 1/n
x:= rand 2. x:= x + rand 3
= Σr: 0,..2· Σs: 0,..3· (x:= r)/2. (x:= x + s)/3
= Σr: 0,..2· Σs: 0,..3· (xʹ = r+s) / 6
= ((xʹ = 0+0) + (xʹ = 0+1) + (xʹ = 0+2) + (xʹ = 1+0) + (xʹ = 1+1) + (xʹ = 1+2)) / 6
= (xʹ=0) / 6 + (xʹ=1) / 3 + (xʹ=2) / 3 + (xʹ=3) / 6
replace one rand with r and one with s Substitution Law
sum
64/77
Random Number Generator
rand n has value r with probability (r: 0,..n) / n
x=x therefore rand n = rand n ?
x+x = 2×x therefore rand n + rand n = 2 × rand n ?
Replace rand n with r: int with distribution (r: 0,..n) / n Replace rand n with r: 0,..n with distribution 1/n
x:= rand 2. x:= x + rand 3
= (xʹ: 0,..2)/2. (xʹ: x+(0,..3))/3
= Σxʹʹ· (xʹʹ: 0,..2)/2 × (xʹ: xʹʹ+(0,..3))/3
= 1/2 × (xʹ: 0,..3)/3 + 1/2 × (xʹ: 1,..4)/3
= (xʹ=0) / 6 + (xʹ=1) / 3 + (xʹ=2) / 3 +
replace rand dependent composition
sum
(xʹ=3) / 6
65/77
Blackjack
You are dealt a card from a deck; its value is in the range 1 to 13 inclusive. You may stop with just one card, or have a second card if you want. Your object is to get a total as near as pos- sible to 14 , but not over 14 . Your strategy is to take a second card if the first is under 7 .
x:= (rand 13) + 1. if x<7 then x:= x + (rand 13) + 1 else ok fi replace rand and ok
= (xʹ: (0,..13)+1)/13. if x<7 then (xʹ: x+(0,..13)+1)/13 else xʹ=x fi replace . and if
= Σxʹʹ· (xʹʹ: 1,..14)/13 × ((xʹʹ<7)×(xʹ: xʹʹ+1,..xʹʹ+14)/13 + (xʹʹ≥7)×(xʹ=xʹʹ))
by several omitted steps
= ((2≤xʹ<7)×(xʹ–1) + (7≤xʹ<14)×19 + (14≤xʹ<20)×(20–xʹ)) / 169
66/77
Player x plays “under n ” and player y plays “under n+1 ”
c:= (rand 13) + 1. d:= (rand 13) + 1.
if c < n then x:=c+d else x:=c fi. if c < n+1 then y:=c+d else y:=c fi. y
∃y· y: S x ∀x· ∃y· y: S x
∀x· S x ⧧ null
P: S S:: P
S is refined by P
74/77
example search for an item in a list
〈L: [*int] → 〈x: int → §n: 0,..#L· Ln = x 〉〉 unimplementable
〈L: [*int] → 〈x: int → if x: L (0,..#L) then §n: 0,..#L· Ln = x else #L,..∞ fi〉〉 if x: L (0,..#L) then §n: 0,..#L· Ln = x else #L,..∞ fi ::
〈i: nat → if x: L (i,..#L) then §n: i,..#L· Ln = x else #L,..∞ fi〉 0
if x: L (i,..#L) then §n: i,..#L· Ln = x else #L,..∞ fi :: if i = #L then #L
else if x = Li then i
else 〈i: nat → if x: L (i,..#L) then §n: i,..#L· Ln = x else #L,..∞ fi〉 (i+1) fi
75/77
recursive timing 〈L → 〈x → 0,..#L+1〉〉 0,..#L+1 :: 〈i → 0,..#L–i+1〉 0
0,..#L–i+1 ::
if i = #L then 0
else if x = Li then 0
else 1 + 〈i → 0,..#L–i+1〉 (i+1) fi fi
1 + 〈i → 0,..#L–i+1〉 (i+1) 1 + (0,..#L–(i+1)+1)
1 + (0,..#L–i)
1,..#L–i+1
0,..#L–i+1
= = = :
76/77
functional versus imperative
same programming steps, different notation
functional programming has Application Axiom 〈v:D·b〉x = (for v substitute x in b)
imperative programming has Substitution Law x:=e.P = (for x substitute e in P)
77/77