311 The specification wait w where w is a length of time, not an instant of time, describes a delay in execution of time w . Formalize and implement it using
(a) the recursive time measure.
§ If t is an extended integer variable and w is an extended natural expression, then define
wait w = t:= t+w and refine it this way:
waitw ⇐ framet·varc:xnat:=w· tʹ′=t+c
tʹ′=t+c ⇐ ifc=0thenokelsec:=c–1. t:=t+1. tʹ′=t+cfi Proof of first refinement:
framet·varc:xnat:=w· tʹ′=t+c
= frame t· ∃c: w· ∃cʹ′: xnat· tʹ′ = t+c
= frame t· tʹ′ = t+w
= t:= t+w
= waitw
Proof of last refinement, first case, assuming the nonlocal variables are x :
c=0 ∧ ok
= c=0 ∧ xʹ′=x ∧ cʹ′=c ∧ tʹ′=t
⇒ tʹ′=t+c
Proof of last refinement, last case:
c>0 ∧ (c:= c–1. t:= t+1. tʹ′ = t+c) ⇒ tʹ′=t+c
expand ok context and specialization
substitution law twice; specialization
(b) the real time measure (assume any positive operation times you need).
§ This time t is an extended real variable and w is a nonnegative extended real expression. The solution can be like part (a), but in the real time measure, we have to account for the time to make the test (which was c=0 in part (a)) and to make a conditional branch, and the time for the assignment (which was c:= c–1 in part (a)), and the time for the recursive call. I’ll use time 1 for all three. As in part (a), we can introduce a counter c initialized to w and count down. But w here is real, not necessarily an integer, so either the test must be c≤0 , or the initial value of c must be
rounded up. I’ll do the latter. Define wait w = t:= t + 3×(ceil w) + 1
and refine it this way:
wait w ⇐ frame t· var c: xnat := ceil w· tʹ′ = t + 3×c + 1
tʹ′ = t + 3×c + 1 ⇐
t:= t+1. if c=0 then ok else t:= t+1. c:= c–1.
Proof of first refinement:
frame t· var c: xnat := ceil w· tʹ′ = t + 3×c + 1
= frame t· ∃c: ceil w· ∃cʹ′: xnat· tʹ′ = t + 3×c + 1
= frame t· tʹ′ = t + 3×(ceil w) + 1
= t:= t + 3×(ceil w) + 1
= waitw
t:= t+1. tʹ′ = t + 3×c + 1 fi cʹ′ is unused; ∃ law
Proof of last refinement, assuming the nonlocal variables are x :
t:= t+1. if c=0 then ok else t:= t+1. c:= c–1. t:= t+1. tʹ′ = t + 3×c + 1 fi
= t:= t+1. if c=0 then ok else tʹ′ = t + 3×c fi
= t:= t+1. if c=0 then cʹ′=c ∧ xʹ′=x ∧ tʹ′=t else tʹ′ = t + 3×c fi
= if c=0 then cʹ′=c ∧ xʹ′=x ∧ tʹ′=t+1 else tʹ′ = t + 3×c + 1 fi
= if c=0 then cʹ′=c ∧ xʹ′=x ∧ tʹ′ = t + 3×c + 1 else tʹ′ = t + 3×c + 1 fi
⇒ tʹ′ = t + 3×c + 1
cʹ′ is unused; ∃ law frame law
substitution law 3 times expand ok substitution law use context c=0 specialize
frame law