ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
Your solution should simulate the following while-loop by primitive recursion:
if n = 0 then return(0) else begin n,a,b := n-1,1,0; while n <> 0 do n,a,b := n-1,a+b,a; return(a) end
Verify your implementation.