252 Let n be a natural variable. Add time according to the recursive measure, and find a finite upper bound on the execution time of
P ⇐ ifn≥2thenn:=n–2. P. n:=n+1. P. n:=n+1elseokfi
§ To ensure that every loop includes a time increment, it is sufficient to put t:= t+1 just before the first call. (But the question isn’t any harder, and the time bound isn’t significantly different, if we put t:= t+1 before both calls.) Because of the two calls, each at approximately the original value of n , I guess the time might be exponential. Actually, it looks just like Fibonacci: the first call is at n–2 , the second is at n–1 . Let’s try
P = tʹ′ ≤ t + 2n
The proof of the refinement will be by cases. First case:
n≥2 ∧ (n:= n–2. t:= t+1. P. n:= n+1. P. n:= n+1)
= n≥2 ∧ (tʹ′ ≤ t + 1 + 2n–2. tʹ′ ≤ t + 2n+1. nʹ′=n+1 ∧ tʹ′=t)
= n≥2 ∧ ∃nʹ′ʹ′, tʹ′ʹ′, nʹ′ʹ′ʹ′, tʹ′ʹ′ʹ′· tʹ′ʹ′ ≤ t + 1 + 2n–2 ∧ tʹ′ʹ′ʹ′ ≤ tʹ′ʹ′ + 2nʹ′ʹ′+1 ∧ nʹ′=nʹ′ʹ′ʹ′+1 ∧ tʹ′=tʹ′ʹ′ʹ′
= n≥2
Oops. The final time seems to be completely arbitrary. The problem is that the first call of P allows n to change arbitrarily, so the last call of P allows t to change arbitrarily. Let’s try again.
P = nʹ′=n ∧ tʹ′ ≤ t + 2n
The proof of the refinement will be by cases. First case:
n≥2 ∧ (n:= n–2. t:= t+1. P. n:= n+1. P. n:= n+1)
= n≥2 ∧ nʹ′=n ∧ tʹ′ ≤ t + 1 + 2n–2 + 2n–1
= n≥2 ∧ nʹ′=n ∧ tʹ′ ≤ t + 1 + 3×2n–2
⇒ n≥2 ∧ nʹ′=n ∧ tʹ′ ≤ t + 2n–2 + 3×2n–2
⇒ nʹ′=n ∧ tʹ′ ≤ t + 2n Last case:
n<2 ∧ ok
= n<2∧nʹ′=n∧tʹ′=t
⇒ nʹ′=n ∧ tʹ′ ≤ t + 2n
when n≥2 , specialize and simplify
and 0≤2n
1 ≤ 2n–2