142 (square) Let s and n be natural variables. Find a specification P such that both the following hold:
sʹ=n2 ⇐ s:=n. P
P ⇐ ifn=0thenokelsen:=n–1. s:=s+n+n. Pfi
This program squares using only addition, subtraction, and test for zero.
§ Looking at the last refinement, I see that it’s a loop, and n gets decreased each iteration, until it is 0 . Also, s gets increased each iteration. So P should have the form
sʹ = s + something
In other words, P says that the final value of s is the current value plus something more. When I am proving the first refinement,
sʹ=n2 ⇐ s:=n. sʹ=s+something I will use the Substitution Law, making it
sʹ=n2 ⇐ sʹ=n+something
Now I see that “something” has to get rid of n and supply n2 . So I’ll try
P =sʹ=s+n2–n
Proof of first refinement, starting with its right side: s:= n. P
= s:= n. sʹ = s + n2 – n
= sʹ=n+n2 –n
= sʹ=n2
Proof of last refinement, starting with its right side: if n=0 then ok else n:= n–1. s:= s+n+n. P fi
= if n=0 then sʹ=s ∧ nʹ=n else n:= n–1. s:= s+n+n. sʹ = s + n2 – n fi
= if n=0 then sʹ=s ∧ nʹ=n else n:= n–1. sʹ = s + n2 + n fi
= if n=0 then sʹ=s ∧ nʹ=n else sʹ = s + (n–1)2 + n – 1 fi
= ifn=0thensʹ=s∧nʹ=nelsesʹ=s+n2 –nfi
⇒ sʹ=s+n2–n =P
I could have used Refinement by Cases to prove the last refinement.
replace P substitution law arithmetic
replace P and ok substitution law substitution law
arithmetic contextinthen-part