156 Let n and r be natural variables in the refinement
P ⇐ if n=1 then r:= 0 else n:= div n 2. P. r:= r+1 fi
Suppose the operations div and + each take time 1 and all else is free (even the call is free). Insert appropriate time increments, and find an appropriate P to express the execution time in terms of
(a) the initial values of the memory variables. Prove the refinement for your choice of P .
§ With time increments added, I must prove
P ⇐ if n=1 then r:= 0 else t:= t+1. n:= div n 2. P. t:= t+1. r:= r+1 fi
How should we choose P ? Execution of P proceeds as follows. If n is initially 0 , then n isdividedby 2,makingitagain 0,andweareinaninfiniteloop. If n is initially positive, then it is repeatedly divided by 2 (rounding down) until it becomes 1 , then r is assigned 0 , then r is incremented as many times as n was divided by 2 . The number of times n is divided by 2 until it becomes 1 is the logarithm (base 2 ) of n . This may not be obvious, so I can easily code this procedure in any implemented programming language I like, and run it for a variety of initial values for n and r and for initial time 0 , and see that the final value of t is 2 × floor (log n) . So P can be
(n=0 ⇒ tʹ=∞) ∧ (n>0 ⇒ tʹ = t + 2 × floor (log n))
But floor is an awkward function to work with, so I’ll get rid of it by replacing the exact time with an upper bound. My choice of P is
(n=0 ⇒ tʹ=∞) ∧ (n>0 ⇒ tʹ ≤ t + 2 × log n)
I prove it in parts (each conjunct separately), and I prove each part by cases. First part, first case:
(n=0 ⇒ tʹ=∞) ⇐ n=1 ∧ (r:= 0) portation
= n=0 ∧ n=1 ∧ (r:= 0)
= ⊥ ∧ (r:= 0) ⇒ tʹ=∞ = ⊥⇒tʹ=∞
=⊤
First part, last case:
⇒ tʹ=∞
(n=0 ⇒ tʹ=∞) ⇐ n⧧1 ∧ (t:= t+1. n:= div n 2. n=0 ⇒ tʹ=∞. t:= t+1. r:= r+1) portation and expand final assignment
=
⇒
=
⇒
=
⇒
(n>0 ⇒ tʹ ≤ t + 2 × log n) ⇐ = n=1 ∧ rʹ=0 ∧ nʹ=n ∧ tʹ=t ⇒ =⊤
=
= =⊤
n=0 ∧ n⧧1 ∧ (t:= t+1. n:= div n 2. n=0 ⇒ tʹ=∞. t:= t+1. rʹ=r+1 ∧ nʹ=n ∧ tʹ=t) tʹ=∞ simplify, and substitution law in two parts n=0 ∧ (div n 2 = 0 ⇒ tʹ=∞. rʹ=r+1 ∧ nʹ=n ∧ tʹ=t+1)
tʹ=∞ eliminate dependent composition n=0 ∧ (∃rʹʹ, nʹʹ, tʹʹ· (div n 2 = 0 ⇒ tʹʹ=∞) ∧ rʹ=rʹʹ+1 ∧ nʹ=nʹʹ ∧ tʹ=tʹʹ+1)
tʹ=∞ context: n=0 n=0 ∧ (∃rʹʹ, nʹʹ, tʹʹ· tʹʹ=∞ ∧ rʹ=rʹʹ+1 ∧ nʹ=nʹʹ ∧ tʹ=tʹʹ+1) ⇒ tʹ=∞ one-point
n=0 ∧ tʹ=∞+1 ⇒ tʹ=∞ Last part, first case:
absorption and specialization
portation and expand assignment context, and log 1 = 0
Last part, last case:
n=1 ∧ (r:= 0) tʹ ≤ t + 2 × log n
=
=
=
= =
= =
(n>0 ⇒ tʹ ≤ t + 2 × log n)
⇐ n 1 ∧ (t:= t+1. n:= div n 2. n>0 ⇒ tʹ ≤ t + 2 × log n. t:= t+1. r:= r+1)
portation and expand final assignment
tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (t:=t+1. n:= div n 2. n>0 ⇒ tʹ ≤ t + 2×log n. t:= t+1. rʹ=r+1 ∧ nʹ=n∧tʹ=t)
substitution law in two parts
tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (div n 2>0 ⇒ tʹ ≤ t+1+ 2 × log(div n 2). rʹ=r+1 ∧ nʹ=n ∧ tʹ=t+1)
eliminate dependent composition
⇐ n>1 ∧ (∃rʹʹ, nʹʹ, tʹʹ· (div n 2>0 ⇒ tʹʹ ≤ t+1+ 2 × log(div n 2))
∧ rʹ=rʹʹ+1 ∧ nʹ=nʹʹ ∧ tʹ=tʹʹ+1) one-point for nʹʹ and tʹʹ
tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (∃rʹʹ· (div n 2>0 ⇒ tʹ ≤ t+2+ 2 × log(div n 2)) ∧ rʹ=rʹʹ+1) distributive
tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (∃rʹʹ: nat· rʹ=rʹʹ+1) ∧ (div n 2>0 ⇒ tʹ ≤ t+2+ 2 × log(div n 2))
in preparation for one-point, rewrite rʹ=rʹʹ+1 and make rʹʹ: nat an explicit conjunct tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (∃rʹʹ: nat· rʹʹ=rʹ–1 ∧ (rʹʹ:nat)) ∧ (div n 2>0 ⇒ tʹ ≤ t+2+ 2 × log(div n 2)) now use one-point
tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (rʹ–1: nat) ∧ (div n 2>0 ⇒ tʹ ≤ t+2+ 2 × log(div n 2))
= tʹ ≤ t + 2 × log n
= tʹ ≤ t + 2 × log n
⇐ n>1 ∧ (rʹ–1: nat) ∧ (div n 2>0 ⇒ tʹ ≤ t + 2 + 2 × log(div n 2)) simplify div n 2>0
⇐ n>1 ∧ rʹ≥1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(div n 2))
increase div n 2 to n/2
this will increase t + 2 + 2 × log(div n 2) this will weaken tʹ ≤ t + 2 + 2 × log(div n 2) this will weaken n>1 ⇒ tʹ ≤ t + 2 + 2 × log(div n 2) this will weaken n>1 ∧ rʹ≥1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(div n 2))
this will strengthen ⇐ tʹ ≤ t + 2 × log n this will strengthen
⇐ tʹ ≤ t + 2 × log n = tʹ ≤ t + 2 × log n =⊤
tʹ ≤ t + 2 × log n
tʹ ≤ t + 2 × log n ⇐ n>1 ∧ rʹ≥1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(div n 2)) so we need to put ⇐ in the left margin ⇐ n>1 ∧ rʹ≥1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(n/2)) drop rʹ≥1 this will weaken n>1 ∧ rʹ≥1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(n/2))
tʹ ≤ t + 2 × log n ⇐ n>1 ∧ rʹ≥1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(n/2)) so again we need to put ⇐ in the left margin ⇐ n>1 ∧ (n>1 ⇒ tʹ ≤ t + 2 + 2 × log(n/2)) discharge and simplify ⇐ n>1 ∧ tʹ ≤ t + 2 × log n specialization
(b) the final values of the memory variables. Prove the refinement for your choice of P .
§ I prove
tʹ = t+2×rʹ ⇐ if n=1 then r:= 0
else t:= t+1. n:= div n 2. tʹ = t+2×rʹ. t:= t+1. r:= r+1 fi
by cases. First case:
tʹ = t+2×rʹ ⇐ n=1 ∧ (r:= 0) expand assignment = tʹ=t+2×rʹ ⇐ n=1∧rʹ=0∧nʹ=n∧tʹ=t
=⊤
Last case:
tʹ = t+2×rʹ ⇐ n⧧1 ∧ (t:= t+1. n:= div n 2. tʹ = t+2×rʹ. t:= t+1. r:= r+1)
expand final assignment
= tʹ = t+2×rʹ ⇐ n⧧1 ∧ (t:=t+1. n:= div n 2. tʹ = t+2×rʹ. t:= t+1. rʹ=r+1 ∧ nʹ=n ∧ tʹ=t) substitution law in two parts
= tʹ = t+2×rʹ ⇐ n⧧1 ∧ (tʹ = t+1+2×rʹ. rʹ=r+1 ∧ nʹ=n ∧ tʹ=t+1) one-point
= tʹ = t+2×rʹ ⇐ n⧧1 ∧ tʹ= t+2+2×(rʹ–1) =⊤