In this section, we will see how to prove the correctness of programs that use recursive functions. We will see that verifying a recursive function is exactly the same as verifying a non-recursive function:

- We must prove a function’s preconditions before calling it (including before making a recursive call)
- After calling a function, we can list the function’s postconditions as premises (including after making a recursive call)
- The function can list its preconditions as premises
- The function must prove its postconditions just before it ends

## Writing a recursive mult function

We know we can multiply two numbers, `x`

and `y`

, using the `*`

operator – `x * y`

. But what if we wanted to find the same result using only addition, not multiplication? Multiplication can be thought of as repeated addition – `x * y`

is really `x + x + ... + x`

, where we add together `y`

total `x`

’s.

We *could* do this repeated addition with a loop (and we will when we introduce loops in section 9.3), but we will use recursion instead. When we write a recursive function, we try to think of two things:

- The
*base case*: the simplest version of the problem that we could immediately solve with no more work. - The
*recursive case*: bigger versions of the problem, where we solve a piece of the problem and then recursively solve a smaller piece

In the case of the multiplication `x * y`

, we have:

- Base case: if
`y`

is 0, we have no work to do. Adding together 0`x`

’s is just 0. - Recursive case: if
`y`

is bigger than 0, we do ONE addition (`x + ...`

) and recursively add the remaining`y - 1`

numbers. (This will become our recursive call.)

With those cases in mind, we can write a recursive `mult`

function:

```
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
def mult(x: Z, y: Z): Z = {
var ans: Z = 0
if (y > 0) {
ans = mult(x, y-1)
ans = ans + x
} else {
//do nothing
}
return ans
}
```

Note that we separated the recursive call (`ans = mult(x, y-1)`

) from adding on the next piece (`ans = ans + x`

). When using Logika, all function calls must go on a separate line by themselves – we can’t combine them with other operations. Also, we included a dummy “else” branch to make the verification simpler.

## Walking through mult

Suppose we call `mult`

as follows:

`var times: Z = mult(4, 2)`

We can trace the recursive calls:

```
times = mult(4, 2)
(x = 4, y = 2)
ans = mult(4, 1) => mult(4, 1)
ans = ans + 4 (x = 4, y = 1)
returns ans ans = mult(4, 0) => mult(4, 0)
ans = ans + 4 (x = 4, y = 0)
returns ans ans = 0
returns 0
```

We start with `mult(4, 2)`

, and then immediately make the recursive call `mult(4, 1)`

, which immediately makes the recursive call `mult(4, 0)`

. That function instance hits the base case and returns 0. We now return back up the chain of function calls – the 0 gets returned back to the `mult(4, 1)`

instance, which adds 4 and then returns 4:

```
=> mult(4, 1)
(x = 4, y = 1)
ans = mult(4, 0) = 0
ans = ans + 4 = 4
returns ans (4)
```

This 4 returns back to the `mult(4, 2)`

instance, which adds another 4 and returns 8:

```
mult(4, 2)
(x = 4, y = 2)
ans = mult(4, 1) = 4
ans = ans + 4 = 8
returns ans (8)
```

We have now backed our way up the chain – the 8 is returned back from the original function call, and `times`

is set to 8.

## mult function contract

Looking at our `mult`

function, we see that the base case is when `y`

is 0 and the recursive case is when `y > 0`

. Clearly, the function is not intended to work for negative values of `y`

. This will be our precondition – that `y`

must be greater than or equal to 0.

Our postcondition should describe what `mult`

is returning in terms of its parameters. In this case, we know that `mult`

is performing a multiplication of `x`

and `y`

using repeated addition. So, our function should ensure that it returns `x*y`

(that `Res[Z] == x*y`

). Here is the function with the function contract:

```
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
def mult(x: Z, y: Z): Z = {
//we still need to add the verification logic blocks
Contract(
Requires( y >= 0 ),
Ensures( Res[Z] == x * y )
)
var ans: Z = 0
if (y > 0) {
ans = mult(x, y-1)
ans = ans + x
} else {
//do nothing
}
return ans
}
```

## Verification in mult

Now that we have our function contract for `mult`

, we must add logic blocks with two things in mind:

- Proving the precondition before a recursive call
- Proving the postcondition before we return from the function

Our recursive call looks like:

`ans = mult(x, y-1)`

Since our precondition is `y >= 0`

, we see that we must prove that what we are passing as the second parameter (`y-1`

, in the case of the recursive call) is greater than or equal to 0. This tells us that before our recursive call, we must have shown exactly: `y-1 >= 0`

. We can finish proving the precondition as follows:

```
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
def mult(x: Z, y: Z): Z = {
//we still need to prove the postcondition
Contract(
Requires( y >= 0 ),
Ensures( Res[Z] == x * y )
)
var ans: Z = 0
if (y > 0) {
Deduce(
1 ( y > 0 ) by Premise, //IF condition is true
2 ( y-1 >= 0 ) by Algebra*(1) //Proves the precondition for the recursive call
)
ans = mult(x, y-1)
ans = ans + x
} else {
//do nothing
}
return ans
}
```

All that remains is to prove the `mult`

postcondition – that we are returning `x*y`

. Since we are returning the variable `ans`

, then we must prove the claim `ans == x*y`

just before our return statement. In order to help with this process, we will need to take advantage of the postcondition after our recursive call. The function promises to return the first parameter times the second parameter, so when we do `ans = mult(x, y-1)`

, we know that `ans == x*(y-1)`

(the first parameter, `x`

, times the second parameter, `y-1`

). Here is the completed verification:

```
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
def mult(x: Z, y: Z): Z = {
//verification complete!
Contract(
Requires( y >= 0 ),
Ensures( Res[Z] == x * y )
)
var ans: Z = 0
if (y > 0) {
Deduce(
1 ( y > 0 ) by Premise, //IF condition is true
2 ( y-1 >= 0 ) by Algebra*(1) //Proves the precondition for the recursive call
)
ans = mult(x, y-1)
Deduce(
1 ( ans == x * (y - 1) ) by Premise, //Postcondition from the recursive call
2 ( ans == x * y - x ) by Algebra*(1)
)
ans = ans + x
Deduce(
1 ( Old(ans) == x * y - x ) by Premise, //Pulled from previous block
2 ( ans == Old(ans) + x ) by Premise, //From the "ans = ans + x" assignment statement
3 ( ans == x + x * y - x ) by Algebra*(1, 2),
4 ( ans == x * y ) by Algebra*(3) //Showed the postcondition for the IF branch
)
} else {
//do nothing in code - but we still do verification
//need to show that postcondition will be correct even if we take this branch
Deduce(
1 ( ¬(y > 0) ) by Premise, //if condition is false
2 ( y >= 0 ) by Premise, //precondition
3 ( y == 0 ) by Algebra*(1, 2),
4 ( ans == 0 ) by Premise, //ans is unchanged
5 ( ans == x * y ) by Algebra*(3, 4) //Showed the postcondition for the ELSE branch
)
}
//Tie together what we learned in both branches
Deduce(
1 ( ans == x*y ) by Premise //shows the postcondition
)
return ans
}
```

## Verification of calling code

Verifying the test code that calls a recursive function works exactly the same way as it does for any other function:

- We must prove the precondition before calling the function
- We can list the postcondition as a premise after calling the function

Suppose we want to test `mult`

as follows:

```
val times: Z = mult(4, 2)
assert(times == 8)
```

We could complete the verification by proving the precondition and then using the postcondition to help us prove the claim in the assert:

```
Deduce(
1 ( 2 >= 0 ) by Algebra*() //proves the precondition
)
val times: Z = mult(4, 2)
Deduce(
1 ( times == 4*2 ) by Premise, //mult postcondition
2 ( times == 8 ) by Algebra*(1) //needed for the assert
)
assert(times == 8)
```

Note that since our second parameter is `2`

, that we must demonstrate exactly `2 >= 0`

to satisfy `mult`

’s precondition. Furthermore, since `mult`

promises to return the first parameter times the second parameter, and since we are storing the result of the function call in the `times`

variable, then we can claim `times == 4*2`

as a premise.