[General boards] [Winter 2019 courses] [Fall 2018 courses] [Summer 2018 courses] [Older or newer terms]

Question from the textbook


This is an example from the textbook about Recursive Program Construction. I don’t understand how the second step of zap_2 was obtained. Specifically, why did x change to be between 2 and 0? And where did t^prime = t + x come from?


Your question is how do we go from
(0) if x=0 then y:= 0 else x:= x–1. t:= t+1. zap_1 fi
(1) 0≤x<2 ⇒ xʹ=yʹ=0 ∧ tʹ=t+x
I admit, it is not obvious. You can test it by choosing various values for x and x’ and t and t’. Here’s how I probably got it. I simplified (0) as much as I could, and got
(2) (x=0 ⇒ x’=y’=0 ∧ t’=t) ∧ (x=1 ⇒ x’=y’=0 ∧ t’=t+1)
Maybe I still didn’t see that (2)=(1) so I found zap_3 and got
(3) (x=0 ⇒ x’=y’=0 ∧ t’=t) ∧ (x=1 ⇒ x’=y’=0 ∧ t’=t+1) ∧ (x=2 ⇒ x’=y’=0 ∧ t’=t+2)
Maybe then I could see that zap_n is
(4) 0≤x<n ⇒ xʹ=yʹ=0 ∧ tʹ=t+x
so I went back and wrote (1) for zap_2. I hope that answers.