Interaction
shared variables
can be read and written by any process (most interaction) difficult to implement
difficult to reason about
interactive variables
can be read by any process, written by only one process (some interaction) easier to implement
easier to reason about
boundary variables
can be read and written by only one process (least interaction) but initial value can be seen by all processes
easiest to implement easiest to reason about
1/29
Interactive Variables
boundary variable var a: T· S = ∃a, aʹ: T· S interactive variable ivar x: T· S = ∃x: time→T· S
The value of variable x at time t is x t
But sometimes we write x for x t , xʹ for x tʹ , xʹʹ for x tʹʹ , …
a:= a+x is really
a:= a + x t
Most laws still work but not the Substitution Law
2/29
Interactive Variables suppose boundary a , b ; interactive x , y ; time t
ok = aʹ=a ∧ bʹ=b ∧ tʹ=t
xʹ=x ∧ yʹ=y means xtʹ=xt ∧ ytʹ=yt
3/29
Interactive Variables suppose boundary a , b ; interactive x , y ; time t
ok = aʹ=a ∧ bʹ=b ∧ tʹ=t a:=e = aʹ=e ∧ bʹ=b ∧ tʹ=t
x:= e
P. Q
P||Q
= aʹ=a ∧ bʹ=b ∧ xʹ=e ∧ (∀tʹʹ· t≤tʹʹ≤tʹ ⇒ yʹʹ=y) ∧ tʹ = t+(the time required to evaluate and store e )
= ∃aʹʹ, bʹʹ, tʹʹ· (substitute aʹʹ, bʹʹ, tʹʹ for aʹ, bʹ, tʹ in P ) ∧ (substitute aʹʹ, bʹʹ, tʹʹ for a, b, t in Q )
= ∃tP, tQ·
(substitute tP for tʹ in P ) ∧ (substitute tQ for tʹ in Q )
∧ tʹ=maxtPtQ
∧ (∀tʹʹ· tP≤tʹʹ≤tʹ ⇒ xtʹʹ=x(tP)) ∧ (∀tʹʹ· tQ≤tʹʹ≤tʹ ⇒ ytʹʹ=y(tQ))
interactive variables of P interactive variables of Q
4/29
Interactive Variables example boundary a , b ; interactive x , y ; extended integer time t
= = =
=
(x:= 2. x:= x+y. x:= x+y) || (y:= 3. y:= x+y) x left, y right, a left, b right (aʹ=a ∧ xtʹ=2 ∧ tʹ=t+1. aʹ=a ∧ xtʹ= xt+yt ∧ tʹ=t+1. aʹ=a ∧ xtʹ= xt+yt ∧ tʹ=t+1)
|| (bʹ=b ∧ ytʹ=3 ∧ tʹ=t+1. bʹ=b ∧ ytʹ= xt+yt ∧ tʹ=t+1)
(aʹ=a ∧ x(t+1)=2 ∧ x(t+2)= x(t+1)+y(t+1) ∧ x(t+3)= x(t+2)+y(t+2) ∧ tʹ=t+3)
|| (bʹ=b ∧ y(t+1)=3 ∧ y(t+2)= x(t+1)+y(t+1) ∧ tʹ=t+2) x(t+1)=2 ∧ x(t+2)= x(t+1)+y(t+1) ∧ x(t+3)= x(t+2)+y(t+2)
∧ y(t+1)=3 ∧ y(t+2)= x(t+1)+y(t+1) ∧ y(t+3)=y(t+2) ∧ aʹ=a ∧ bʹ=b ∧ tʹ=t+3
x(t+1)=2 ∧ x(t+2)=5 ∧ x(t+3)=10 ∧ y(t+1)=3 ∧ y(t+2)=y(t+3)=5 ∧ aʹ=a ∧ bʹ=b ∧ tʹ=t+3
5/29
Thermostat
thermometer || control || thermostat || burner
inputs to the thermostat:
• real temperature , which comes from the thermometer and indicates the actual
temperature.
• real desired , which comes from the control and indicates the desired temperature.
• binary flame , which comes from a flame sensor in the burner and indicates whether
there is a flame.
outputs of the thermostat:
• binary gas ; assigning it ⊤ turns the gas on and ⊥ turns the gas off.
• binary spark ; assigning it ⊤ causes sparks for the purpose of igniting the gas.
6/29
Heat is wanted when the actual temperature falls ε below the desired temperature, and not wanted when the actual temperature rises ε above the desired temperature, where ε is small enough to be unnoticeable, but large enough to prevent rapid oscillation. To obtain heat, the spark should be applied to the gas for at least 1 second to give it a chance to ignite and to allow the flame to become stable. But a safety regulation states that the gas must not remain on and unlit for more than 3 seconds. Another regulation says that when the gas is shut off, it must not be turned on again for at least 20 seconds to allow any accumulated gas to clear. And finally, the gas burner must respond to its inputs within 1 second.
thermostat = (gas:= ⊥ || spark:= ⊥). GasOff
GasOff =
if temperature < desired – ε
then (gas:= ⊤ || spark:= ⊤ || tʹ ≥ t+1) ∧ tʹ ≤ t+3. spark:= ⊥. GasOn
else ((frame gas, spark· ok) || tʹ≥t) ∧ tʹ ≤ t+1. GasOff fi
if temperature < desired + ε ∧ flame
then ((frame gas, spark· ok) || tʹ≥t) ∧ tʹ ≤ t+1. GasOn
else (gas:= ⊥ || (frame spark· ok) || tʹ ≥ t+20) ∧ tʹ ≤ t+21. GasOff fi
GasOn =
7/29
Channel c is described by
message script Mc
time script Tc read cursor rc write cursor wc
string constant
string constant
extended natural variable extended natural variable
Communication Channels
M = 6 ; 4 ; 7 ; 1 ; 0 ; 3 ; 8 ; 9 ; 2 ; 5 ;... T = 3 ;5 ;5 ;20;25;28;31;31;45;48;...
↑↑
rw
8/29
Input and Output
c!e = Mw=e ∧ Tw=t ∧ (w:=w+1) c! = Tw=t ∧ (w:=w+1)
c? = r:=r+1
c = Mr–1 √c = Tr ≤ t
M = 6 ; 4 ; 7 ; 1 ; 0 ; 3 ; 8 ; 9 ; 2 ; 5 ;... T = 3 ;5 ;5 ;20;25;28;31;31;45;48;...
↑↑
rw
9/29
Input and Output
c!e = Mw=e ∧ Tw=t ∧ (w:=w+1) c! = Tw=t ∧ (w:=w+1)
c? = r:=r+1
c = Mr–1 √c = Tr ≤ t
if √key
then key?.
if key=“y”
then screen! “If you wish.”
else screen! “Not if you don't want.” fi
else screen! “Well?” fi
10/29
Input and Output
Repeatedly input numbers from channel c , and output their doubles on channel d . S = ∀n: nat· Mdwd+n = 2 × Mcrc+n
S ⇐ c?. d! 2×c. S proof
c?. d! 2×c. S
= rc:= rc+1. Mdwd = 2 × Mcrc–1 ∧ (wd:= wd+1). S
= Mdwd = 2 × Mcrc ∧ ∀n: nat· Mdwd+1+n = 2 × Mcrc+1+n
= ∀n: nat· Mdwd+n = 2 × Mcrc+n =S
11/29
Communication Timing real time need to know implementation
transit time input and output take time 0 communication transit takes time 1
input c? becomes t:= max t (Tcrc + 1). c? check √c becomes Tcrc + 1 ≤ t
12/29
Communication Timing
W = t:= max t (Tr + 1). c?
= wait (if necessary) for input and then read it
W ⇐ if√cthenc?elset:=t+1. Wfi proof
if√cthenc?elset:=t+1. Wfi
= if Tr + 1 ≤ t then c? else t:= t+1. t:= max t (Tr + 1). c? fi
= if Tr + 1 ≤ t then t:= t. c? else t:= max (t+1) (Tr + 1). c? fi
= if Tr + 1 ≤ t then t:= max t (Tr + 1). c? else t:= max t (Tr + 1). c? fi =W
13/29
Recursive Communication
dbl = c?. d! 2×c. t:= t+1. dbl weakest solution
∀n: nat· Mdwd+n = 2 × Mcrc+n ∧ Tdwd+n = t+n strongest implementable solution
(∀n: nat· Mdwd+n = 2 × Mcrc+n ∧ Tdwd+n = t+n) ∧ rcʹ=wdʹ=tʹ=∞ ∧ wcʹ=wc ∧ rdʹ=rd
strongest solution
⊥
∀n: nat· Mdwd+n = 2 × Mcrc+n ∧ Tdwd+n= t+n ⇐ dbl dbl ⇐ c?. d! 2×c. t:= t+1. dbl
14/29
dbl0 =⊤
Recursive Construction
dbl1 =
= rc:= rc+1. Mdwd = 2 × Mcrc–1 ∧ Tdwd = t ∧ (wd:= wd+1). t:= t+1. ⊤
= Mdwd = 2 × Mcrc ∧ Tdwd = t
c?. d! 2×c. t:= t+1. dbl0
dbl2 =
= rc:= rc+1. Mdwd = 2 × Mcrc–1 ∧ Tdwd = t ∧ (wd:= wd+1). t:= t+1.
Mdwd = 2 × Mcrc ∧ Tdwd = t
= Mdwd = 2 × Mcrc ∧ Tdwd = t ∧ Mdwd+1 = 2×Mcrc+1 ∧ Tdwd+1 = t+1
c?. d! 2×c. t:= t+1. dbl1
dbl∞ =
∀n: nat· Mdwd+n = 2 × Mcrc+n ∧ Tdwd+n = t+n
15/29
x0in x0ack
x1in x1ack
x0req x0out
x1req x1out
Monitor
x
monitor =
(√x0in ∨ Tx0inrx0in = m) ∧ (x0in?. x:= x0in. x0ack!) ∨ (√x1in ∨ Tx1inrx1in = m) ∧ (x1in?. x:= x1in. x1ack!)
∨ (√x0req ∨ Tx0reqrx0req = m) ∧ (x0req?. x0out! x) ∨ (√x1req ∨ Tx1reqrx1req = m) ∧ (x1req?. x1out! x). monitor
16/29
Monitor
x0in x0req x0ack x0out
x1in x1req x1ack x1out
monitor ⇐
if √x0in then x0in?. x:= x0in. x0ack! else ok fi. if √x1in then x1in?. x:= x1in. x1ack! else ok fi. if √x0req then x0req?. x0out! x else ok fi.
if √x1req then x1req?. x1out! x else ok fi.
t:= t+1. monitor
x
17/29
c! 2 || (c?. x:= c)
= Mw = 2 ∧
= Mw = 2 ∧
c! 1. (c! 2
(w:= w+1) || (r:= r+1. x:= Mr–1 ) wʹ = w+1 ∧ rʹ = r+1 ∧ xʹ = Mr
|| (c?. x:= c)). c?
Communicating Processes
channel declaration
chan c: T· P
= ∃Mc: ∞*T· ∃Tc: ∞*xnat· var rc , wc: xnat := 0· P
18/29
ignoring time
chan c: int· c! 2 || (c?. x:= c)
= ∃M: ∞*int· ∃T: ∞*xnat· var r, w: xnat := 0·
xʹ = Mr ∧ Mw = 2 ∧ rʹ = r+1 ∧ wʹ = w+1 ∧ (other variables unchanged)
= ∃M: ∞*int· ∃T: ∞*xnat· var r, w: xnat·
xʹ = M0 ∧ M0 = 2 ∧ rʹ=1 ∧ wʹ=1 ∧ (other variables unchanged)
= xʹ=2 ∧ (other variables unchanged)
= x:= 2
including time
chan c: int· c! 2 || (t:= max t (Tr + 1). c?. x:= c)
= xʹ=2 ∧ tʹ = t+1 ∧ (other variables unchanged)
19/29
chan c: int· t:= max t (Tr + 1). c?. c! 5
= ∃M: ∞*int· ∃T: ∞*xnat· var r, w: xnat := 0·
t:= max t (Tr + 1). r:= r+1. Mw = 5 ∧ Tw = t ∧ (w:= w+1)
= ∃M: ∞*int· ∃T: ∞*xnat· ∃r, rʹ, w, wʹ: xnat·
Deadlock
r:= 0. w:= 0. t:= max t (Tr + 1). r:= r+1. Mw = 5 ∧ Tw = t ∧ rʹ=r ∧ wʹ = w+1 ∧
= ∃M: ∞*int· ∃T: ∞*xnat· ∃r, rʹ, w, wʹ: xnat· M0 = 5 ∧ T0 = max t (T0 + 1) ∧ rʹ=1 ∧
tʹ=t
wʹ=1 ∧
tʹ = max t (T0 + 1)
= tʹ=∞
20/29
Deadlock
chan c, d: int· (c?. d! 6) || (d?. c! 7)
chan c, d: int· (t:= max t (Tcrc + 1). c?. d! 6) || (t:= max t (Tdrd + 1). d?. c! 7) = ∃Mc, Md: ∞*int· ∃Tc, Td: ∞*xnat· ∃rc, rcʹ, wc, wcʹ, rd, rdʹ, wd, wdʹ: xnat·
Md0 = 6 ∧ Mc0 = 7 ∧ rcʹ = wcʹ = rdʹ = wdʹ = 1
∧ Tc0 = max t (Td0 + 1) ∧ Td0 = max t (Tc0 + 1)
∧ tʹ = max (max t (Td0 + 1)) (max t (Tc0 + 1))
= tʹ=∞
21/29
Input on channel a : a0 a1 a2 ... Input on channel b : b0 b1 b2 ... Output on channel c : c0 c1 c2 ...
A1 = a1 + a2×x + a3×x2 + ...
A2 = a2 + a3×x + a4×x2 + ...
A = a0 + a1×x + a2×x2 + ... B = b0 + b1×x + b2×x2 + ... C = c0 + c1×x + c2×x2 + ...
B1 = b1 + b2×x + b3×x2 + ... B2 = b2 + b3×x + b4×x2 + ...
Power Series Multiplication
C = A × B = a0×b0 + (a0×b1 + a1×b0)x + (a0×B2 + A1×B1 + A2×b0)×x2 〈chanc:rat→C=A×B〉c ⇐ (a?||b?). c!a×b.
var a0: rat := a· var b0: rat := b· chan d: rat· 〈chan c: rat → C = A×B〉 d
|| ((a?||b?). c!a0×b+a×b0. C=a0×B+D+A×b0) C=a0×B+D+A×b0 ⇐ (a?||b?||d?). c!a0×b+d+a×b0. C=a0×B+D+A×b0
22/29
Binary Theory Number Theory Bunches
Functions Specification
Program Development Space Calculation Scope
Data Structures Control Structures
laws
Character Theory
Sets
Quantifiers
Refinement
Time Calculation
maximum space
variable declaration
array element assignment
while-loop loop with exit
Review
proof
Strings
Lists
exact postcondition recursive time
exact precondition real time
average space frame
for-loop
23/29
Time Dependence
Assertions
Subprograms
Probabilistic Programming Functional Programming Recursive Data Definition Recursive Program Definition Theory Design and Implementation Data Transformation
Independent Composition Interactive Variables
wait
checking backtracking function procedure random number generator
Review
construction construction data theory
sequential to parallel transformation Communication Channels
refinement induction induction program theory
timing
24/29
Disjoint Composition
Independent composition P||Q requires that P and Q have no variables in common, although each can make use of the initial values of the other's variables by making a private copy. An alternative, let's say disjoint composition, is to allow both P and Q to use all the variables with no restrictions, and then to choose disjoint sets of variables v and w and define
P |v|w| Q = (P. vʹ=v) ∧ (Q. wʹ=w)
(a) Prove that if P and Q are implementable specifications, then P |v|w| Q is
implementable.
Application Law 〈v→b〉 a = (substitute a for v in b ) Let the remaining variables (if any) be x .
25/29
Disjoint Composition
P. vʹ=v
= ∃vʹʹ, wʹʹ, xʹʹ· 〈vʹ, wʹ, xʹ → P〉 vʹʹ wʹʹ xʹʹ ∧ vʹ=vʹʹ
= ∃wʹʹ, xʹʹ· 〈vʹ, wʹ, xʹ → P〉 vʹ wʹʹ xʹʹ
= ∃wʹ, xʹ· 〈vʹ, wʹ, xʹ → P〉 vʹ wʹ xʹ
= ∃wʹ, xʹ· P
Q. wʹ=w
= ∃vʹ, xʹ· Q
P|v|w|Q = (P. vʹ=v)∧(Q. wʹ=w) = (∃wʹ,xʹ·P)∧(∃vʹ,xʹ·Q)
expand dependent composition
one-point vʹʹ rename wʹʹ, xʹʹ to wʹ, xʹ apply
26/29
Disjoint Composition
( P |v|w| Q is implementable)
= ∀v, w, x· ∃vʹ, wʹ, xʹ· P |v|w| Q
= ∀v, w, x· ∃vʹ, wʹ, xʹ· (∃wʹ, xʹ· P) ∧ (∃vʹ, xʹ· Q)
= ∀v, w, x· ∃vʹ, wʹ· (∃wʹ, xʹ· P) ∧ (∃vʹ, xʹ· Q)
= ∀v, w, x· ∃vʹ· ∃wʹ· (∃wʹ, xʹ· P) ∧ (∃vʹ, xʹ· Q)
= ∀v, w, x· ∃vʹ· (∃wʹ, xʹ· P) ∧ (∃wʹ· ∃vʹ, xʹ· Q)
= ∀v, w, x· (∃vʹ· ∃wʹ, xʹ· P) ∧ (∃wʹ· ∃vʹ, xʹ· Q)
= ∀v, w, x· (∃vʹ, wʹ, xʹ· P) ∧ (∃vʹ, wʹ, xʹ· Q)
= (∀v, w, x· ∃vʹ, wʹ, xʹ· P) ∧ (∀v, w, x· ∃vʹ, wʹ, xʹ· Q)
= ( P is implementable) ∧ ( Q is implementable)
definition of implementable use previous result
identity for xʹ distribution (factoring)
distribution (factoring)
splitting law definition of implementable
27/29
Disjoint Composition
Independent composition P||Q requires that P and Q have no variables in common, although each can make use of the initial values of the other's variables by making a private copy. An alternative, let's say disjoint composition, is to allow both P and Q to use all the variables with no restrictions, and then to choose disjoint sets of variables v and w and define
P |v|w| Q = (P. vʹ=v) ∧ (Q. wʹ=w)
(b) Describe how P |v|w| Q can be executed.
Make a copy of all variables. Execute P using the original set of variables and in parallel execute Q using the copies. Then copy back from the copy w to the original w . Then throw away the copies.
28/29
Disjoint Composition
Independent composition P||Q requires that P and Q have no variables in common, although each can make use of the initial values of the other's variables by making a private copy. An alternative, let's say disjoint composition, is to allow both P and Q to use all the variables with no restrictions, and then to choose disjoint sets of variables v and w and define
P |v|w| Q = (P. vʹ=v) ∧ (Q. wʹ=w)
(b) Describe how P |v|w| Q can be executed.
P |v|w| Q ⇐ var cv:=v· var cw:=w· var cx:=x· (P||〈v,w,x,vʹ,wʹ,xʹ→Q〉cvcwcxcvʹcwʹcxʹ). w:=cw
29/29