1. ## Program Correctness Problem

*** It's not necessarily that this problem is overly difficult but I was just wondering if anyone could help show the clear and correct way to solve this by use of a loop invariant and induction.***

*Use induction to prove the following program to compute x*y is correct given the initial assertion that x is a non-negative integer and the final asseration that the value returned from mult(x,y) is x*y.

procedure mult(x,y)

if(x==0) then return 0
else return y + mult(x-1, y)

2. Originally Posted by fusion1455
*** It's not necessarily that this problem is overly difficult but I was just wondering if anyone could help show the clear and correct way to solve this by use of a loop invariant and induction.***

*Use induction to prove the following program to compute x*y is correct given the initial assertion that x is a non-negative integer and the final asseration that the value returned from mult(x,y) is x*y.

procedure mult(x,y)

if(x==0) then return 0
else return y + mult(x-1, y)
base case: x=0

the procedure returns 0 which is indeed x*y

inductive step: pass x+1,y

as x+1 is not 0, follow the else statement. return y plus whatever mult(x+1-1,y) returns. the nested mult() returns 0 so the parent procedure returns y which is y greater than what x*y returned in the base case.