Chapter 9

Functions and Loops

Programming Logic: Functions and Loops

In this chapter, we will continue our unit on programming logic and will learn how to prove the correctness of programs involving functions, loops, and recursion.

Functions

A function in Scala is analogous to a method in Java or C# – it is a named body of commands that does significant work. It may take one or more parameters and/or return a value. Recall the syntax for a function in Scala:

def functionName(paramList): returnType = {

}

We will use the keyword Unit (like void in other languages) for a function that does not return a value. If a function has a non-Unit return type, then all paths through the function must end in a return statement:

return expression

Where expression is a variable, literal, or expression matching returnType.

Function contracts

In order to prove the correctness of a function, it must include a function contract just inside the function header. This function contract specifies what we need to know to use the function correctly. While we will use these specifications to help us prove correctness, they are good to include in ANY library function that will be used by someone else (even more informally in other languages). The person/program who calls the function is not supposed to read the function’s code to know how to use the function. A function contract shows them what parameters to pass (including what range of values are acceptable), what the function will return in terms of the parameter, and whether/how the function will modify things like sequences (arrays/lists in other languages) or global variables.

Here is the syntax for a function contract in Logika:

Contract(
    Requires (  preconditions   ),
    Ensures (   postconditions  )
)

Here is a summary of the different function contract clauses:

Requires: lists the preconditions for the function in a comma-separated list. If there are no preconditions, we can skip this clause.
Ensures: lists the postconditions for the function in a comma-separated list.

Preconditions

The preconditions for a function are requirements the function has in order to operate correctly. Generally, preconditions constrain the values of the parameters and/or global variables. For example, this function returns the integer division between two parameters. The function can only operate correctly when the denominator (the second parameter, b) is non-zero:

def div(a: Z, b: Z) : Z =  {
    Contract(
        Requires (  b != 0  ),
        ...
    )

    val ans: Z = a/b
    return ans
}

Logika will display an error if any preconditions are not proven before calling a function. Because we are required to prove the preconditions before any function call, the function itself can list the preconditions as premises in a proof block just after the function contract:

def example(a: Z, b: Z) : Z =  {
    Contract(
        Requires (  Precondition1, Precondition2, ...),
        ...
    )

    //we can list the preconditions as premises
    Deduce(
        1 ( precondition1   )   by Premise,
        2 ( precondition2   )   by Premise
        ...
    )

    ...
}

Postconditions

The postconditions of a function state what the function has accomplished when it terminates. In particular, postconditions should include:

A formalization of what the function promises to return in terms of the parameters/global variables. We use the keyword Res[returnType] to refer to the object returned by the function (we will only use this keyword in the function contract). For example, in a function that returns an integer (Z), we can use the keyword Res[Z] in a postcondition to refer to the return value.
A description of how any global variables and/or sequence parameters will be modified by the function (we will not use global variables or sequences until chapter 10).

For example, the div function above should promise to return the integer division of its two parameters, like this:

def div(a: Z, b: Z) : Z =  {
    Contract(
        Requires(   b != 0  ),
        Ensures(    Res[Z] == a/b   )
    )

    val ans: Z = a/b
    return ans
}

In order to prove a postcondition involving the return value, we must have proof blocks just before returning that demonstrate each postcondition claim, using the variable name being returned instead of the Res[returnType] keyword. In the example above, since we are returning a variable named ans, then we must prove the claim ans == a/b in order to satisfy the postcondition. We can complete the verification of the div function as follows:

def div(a: Z, b: Z) : Z =  {
    Contract(
        Requires(   b != 0  ),
        Ensures(    Res[Z] == a/b   )
    )

    val ans: Z = a/b

    Deduce(
        1 ( b != 0      )   by Premise, //precondition (needed for division)
        2 ( ans == a/b  )   by Premise  //satisifes the postcondition
                                        //(from the "ans = a/b" assignment)
    )

    return ans
}

Logika will display an error if postconditions are not proven before leaving a function. Because we are required to prove the postconditions before the function ends, any calling code can list those postconditions as premises after calling the function. We will see this in more detail in the next section.

Work of the calling code

We saw above that when writing code that calls a function, we must PROVE the preconditions before the function call (since the function requires that we meet those preconditions in order to work correctly). After the function terminates, the calling code can list the function’s postconditions as PREMISES (since the function ensured that certain things would happen).

The “calling code” in Scala goes outside of any function definition. Typically, I place the calling code at the bottom of the Scala file, after all functions. This is the code executed first by Scala, just like in Python programs.

Proving preconditions

Suppose we wish to call the div function to divide two numbers:

val x: Z = 10
val y: Z = 2

val num: Z = div(x, y)

If we included that calling code in a file with our div function, we would see an error that we had not yet proved the precondition. To prove each precondition, we must have a proof block just before the function call that demonstrate each precondition claim, using value being passed instead of the parameter name. Since we are passing the value y as our second parameter, and since the div function requires that b != 0 (where b is the second parameter), then we must demonstrate that y != 0:

val x: Z = 10
val y: Z = 2

Deduce(
    1 ( x == 10     )   by Premise,     //from the "x = 10" assignment
    2 ( y == 2      )   by Premise,     //from the "y = 2" assignment
    3 ( y != 0      )   by Algebra*(2)  //satisfies the precondition for div
)

val num: Z = div(x, y)

Note that Logika is picky about proving the precondition using EXACTLY the value being passed for the corresponding parameter. For example, suppose instead that we wanted to divide x-1 and y+1:

val x: Z = 10
val y: Z = 2

Deduce(
    1 ( x == 10     )   by Premise,     //from the "x = 10" assignment
    2 ( y == 2      )   by Premise,     //from the "y = 2" assignment
    3 ( y != 0      )   by Algebra*(2)  //NO! precondition is not satisfied!
)

val num: Z = div(x-1, y+1)

If we made no changes to our logic block, Logika would complain that we had not satisfied the precondition. And indeed we haven’t – while we’ve shown that y isn’t 0, we haven’t shown that our second parameter y+1 isn’t 0. Here is the correction:

val x: Z = 10
val y: Z = 2

Deduce(
    1 ( x == 10     )   by Premise,     //from the "x = 10" assignment
    2 ( y == 2      )   by Premise,     //from the "y = 2" assignment
    3 ( y+1 != 0    )   by Algebra*(2)  //Yes! Satisfies the precondition for our second parameter (y+1)
)

val num: Z = div(x-1, y+1)

Using postconditions

Recall that since the function is ensuring that it will do/return specific things (its postconditions), then the calling code can list those postconditions as premises after the function call. If a postcondition uses the keyword Res[returnType], then the calling code can list exactly that postcondition using whatever variable it used to store the return value in place of Res[returnType] and using whatever values were passed in place of the parameter names. In the div example above where we divide x-1 by y+1, the calling code stores the value returned by div in a variable called num. Since the div postcondition is result == a/b, then we can claim the premise num == (x-1)/(y+1):

val x: Z = 10
val y: Z = 2

Deduce(
    1 ( x == 10     )   by Premise,     //from the "x = 10" assignment
    2 ( y == 2      )   by Premise,     //from the "y = 2" assignment
    3 ( y+1 != 0    )   by Algebra*(2)  //Yes! Satisfies the precondition for our second parameter (y+1)
)

val num: Z = div(x-1, y+1)

Deduce(
    1 ( num == (x-1)/(y+1)  )   by Premise  //postcondition of div
)

We know from looking at this example that (x-1)/(y+1) is really 9/3, which is 3. We would like to be able to assert that num, the value returned from div, equals 3. We can do this by adding a few more steps to our final proof block, plugging in the values for x and y and doing some algebra:

val x: Z = 10
val y: Z = 2

Deduce(
    1 ( x == 10     )   by Premise,     //from the "x = 10" assignment
    2 ( y == 2      )   by Premise,     //from the "y = 2" assignment
    3 ( y+1 != 0    )   by Algebra*(2)  //Yes! Satisfies the precondition for our second parameter (y+1)
)

val num: Z = div(x-1, y+1)

Deduce(
    1 ( num == (x-1)/(y+1)  )   by Premise,     //postcondition of div
    2 ( x == 10             )   by Premise,     //previous variable assignment
    3 ( y == 2              )   by Premise,     //previous variable assignment
    4 ( num == 9/3          )   by Algebra*(1,2,3),
    5 ( num == 3            )   by Algebra*(4)  //needed for assert 
)

assert(num == 3)

Using a function contract and our deduction rules, we have PROVED that the div function will return 3 in our example (without needing to test the code at all).

Examples

In this section, we will see two completed examples of Logika programs with a function and calling code.

Example 1

In this example, we write a plusOne function that takes a non-negative parameter and returns one more than that parameter:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._

def plusOne(n: Z): Z = {
    Contract(
        Requires(   n >= 0  ),
        Ensures(
            Res[Z] == n + 1,
            Res[Z] > 0
        )
    )

    val answer: Z = n + 1
  
    Deduce(
        1  (    n >= 0          )   by Premise,
        2  (    answer == n + 1 )   by Premise,
        3  (    answer > 0      )   by Algebra*(1, 2)
    )

    return answer
}

////////// Test code ///////////////

var x: Z = 5
Deduce(
    1  (    x == 5  )   by Premise,
    2  (    x >= 0  )   by Algebra*(1)
)

var added: Z = plusOne(x)

Deduce(
    1  (    x == 5                  ) by Premise,
    2  (    added == x + 1          ) by Premise,
    3  (    added > 0               ) by Premise,
    4  (    added == 6              ) by Algebra*(1, 2),
    5  (    added == ∧ & added > 0  ) by AndI(4, 3)
)
assert(added == 6 ∧ added > 0)

var x: Z = 5

Deduce(
    1 (     x == 5      )   by Premise,     //from the "x=5" assignment
    2 (     x >= 0      )   by Algebra*(1)  //proves the plusOne precondition
)

var added: Z = plusOne(x)

Deduce(
    //I can list the postcondition (what is returned) as a premise
    1 (     x == 5                  )   by Premise, //x is unchanged 
    2 (     added == x+1            )   by Premise, //plusOne postcondition 1
    3 (     added > 0               )   by Premise, //plusOne postcondition 2
    4 (     added == 6              )   by Algebra*(1,2),
    5 (     added == 6 ∧ added > 0  )   by AndI(4,3)
)

assert(added == 6 ∧ added > 0)

Note that when we have more than one postcondition, we must prove all postconditions inside the function, and we can list all postconditions as premises in the calling code after the function call.

Example 2

In this example, we write a findMax function that returns the biggest between two integer parameters. This is very similar to an example from section 8.7, which used an if/else statement to find the max. In that example, our assert that we had indeed found the max was: assert((max >= x & max >= y) & (max == x | max == y)). We will see that our postconditions for findMax come directly from the different claims in that assert. In our calling code, we call findMax with num1 (which has the value 3) and num2 (which has the value 2). We are able to prove that findMax returns 2:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._

//find the max between x and y
def findMax(x: Z, y: Z): Z = {
    Contract(
        //no precondition needed
        Ensures(
            Res[Z] >= x,                //postcondition 1
            Res[Z] >= y,                //postcondition 2
            Res[Z] == x v Res[Z] == y   //postcondition 3
        )
    )

    var max: Z = 0

    if (x > y) {
        max = x

        Deduce(
            1 (     max == x    )   by Premise,
            2 (     max >= x    )   by Algebra*(1),     //build to postcondition 1
            3 (     x > y       )   by Premise,         //IF condition is true
            4 (     max >= y    )   by Algebra*(1,3)    //build to postcondition 2
        )

    } else {
        max = y

        Deduce(
            1 (     max == y    )   by Premise,
            2 (     ¬(x > y)    )   by Premise,         //IF condition is false
            3 (     x <= y      )   by Algebra*(2),
            4 (     max >= x    )   by Algebra*(1, 2),  //build to postcondition 1
            5 (     max >= y    )   by Algebra*(1)      //build to postcondition 2
        )
    }

    //prove the postconditions
    Deduce(
        //true in both the if and the else
        1 (     max >= x            )   by Premise,     //proves postcondition 1 
        2 (     max >= y            )   by Premise,     //proves postcondition 2

        //first was true in if, second true in else
        3 (     max == x v max == y )   by Premise     //proves postcondition 3
    )

    return max
}

////////////// Test code /////////////////

val num1: Z = 3
val num2: Z = 2

//findMax has no preconditions, so nothing to prove here

val biggest: Z = findMax(num1, num2)

Deduce(
    1 (     biggest >= num1                     )   by Premise,     //findMax postcondition 1
    2 (     biggest >= num2                     )   by Premise,     //findMax postcondition 2
    3 (     biggest == num1 v biggest == num2   )   by Premise,     //findMax postcondition 3

    //pull in the initial values
    4 (     num1 == 3                           )   by Premise,
    5 (     num2 == 2                           )   by Premise,

    6 (     biggest >= 3                        )   by Algebra*(1, 4),
    7 (     biggest >= 2                        )   by Algebra*(2, 5),
    8 (     biggest == 3 v biggest == num2      )   by Subst_<(4, 3),
    9 (     biggest == 3 v biggest == 2         )   by Subst_<(5, 8),

    //OR-elimination
    10 SubProof(
        11  Assume( biggest == 3 ) 
    ),
    12 SubProof(
        13  Assume( biggest == 2 ) 
        14 (    ¬(biggest >= 3)                 )   by Algebra*(13),
        15 (    F                               )   by NegE(6, 14),
        16 (    biggest == 3                    )   by BottomE(15)
    ),
    17 (        biggest == 3                    )   by OrE(9,10,12) //needed for assert
)

assert(biggest == 3)

Recursion

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.

Loops

A loop is a command that restarts itself over and over while its loop condition remains true. Loops are trickier to analyze than if/else statements, because we don’t know how many times the loop will execute. The loop condition might be initially false, in which case we would skip the body of the loop entirely. Or, the loop might go through 1 iteration, or 10 iterations, or 100 iterations…we don’t know. We want a way to analyze what we know to be true after the loop ends, regardless of how many iterations it makes.

The only loop available in Logika is a while loop, which behaves in the same way as while loops in other languages. If the loop condition is initially false, then the body of the while loop is skipped entirely. If the loop condition is initially true, then we execute the loop body and then recheck the condition. This continues until the loop condition becomes false.

Here is the syntax of a Scala while loop:

while (condition) {
   //body of loop
}

Loop invariants

Our solution to analyzing loops despite not knowing the number of iterations is a tool called a loop invariant. The job of the loop invariant is to summarize what is always true about the loop. Often, the loop invariant describes the relationship between variables and demonstrates how much progress the loop has made. Sometimes the loop invariant also contains claims that certain variables will always stay in a particular range.

Whatever we choose as the loop invariant, we must be able to do the following:

Prove the loop invariant is true before the loop begins
Assume the loop invariant is true at the beginning of an iteration, and prove that the invariant is STILL true at the end of the iteration

Loop invariants and mathematical induction

The process of proving the correctness of loop invariants is very similar to a mathematical induction proof. We must prove the loop invariant is true before the loop begins, which is analogous to the base case in mathematical induction. The process of assuming the invariant is true at the beginning of an iteration and proving that it is still true at the end of an iteration is just like mathematical induction’s inductive step.

If we prove those two things about our invariant, we can be certain the invariant will still hold after the loop terminates. Why? For the same reason mathematical induction proves a property for a general $n$:

We know the invariant holds before the loop begins
Because the invariant holds before the loop begins, we are sure it holds at the beginning of the first iteration
Because we’ve proved the invariant still holds at the end of each iteration, we’re sure it still holds at the end of the first iteration
Because we’re sure it still holds at the end of the first iteration, we know it holds at the beginning of the second iteration
Because we’ve proved the invariant still holds at the end of each iteration, we’re sure it still holds at the end of the second iteration …
We’re sure the invariant still holds at the end of each iteration, including the end of the LAST iteration. Thus we’re certain the invariant holds just after the loop ends.

Loop invariant block syntax

In Logika, we will write a loop invariant block to describe our loop invariants. This block will go just inside the loop, before the loop body:

while (condition) {
    Invariant(
        Modifies(comma-separated list of variables),
        Invariant_1,
        Invariant_2,
        ...
    )

    //loop body
}

Here is a summary of the different loop invariant clauses:

Modifies: uses a comma-separated list to name each variable whose value changes in the loop body
Invariant_i: lists an invariant for the function. If we have multiple invariants, we can list them on separate lines (Invariant_1, Invariant_2, etc.)

Example: loop invariant block for a multiplication loop

Suppose we have the following loop to multiply two numbers, x and y, using repeated addition. (This is very similar to our mult function from section 9.2, except it does the additions using a loop instead of using recursion):

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

val x: Z = Z.read()
val y: Z = Z.read()

var sum: Z = 0
var count: Z = 0

while (count != y) {
    sum = sum + x
    count = count + 1
}

//now sum is x*y

Before writing the loop invariant block, let’s make a table showing the values of different variables at different points in the loop:

Variable	Before loop	After iteration 1	After iteration 2	After iteration 3	…	After iteration y
`count`	0	1	2	3	…	y
`sum`	$0 (= 0*x)$	$x (= 1*x)$	$x + x (= 2*x)$	$x + x + x (= 3*x)$	…	$x + x + ... + x (= y*x)$

Before the loop begins, we’ve added 0 $x$’s together, so the sum is 0. After the first iteration, we’ve added 1 $x$ together, so the sum is $x$. After the second iteration, we’ve added 2 $x$’s together, so the sum is $x + x$ which is really $2 * x$. This continues until after the y-th iteration, when we’ve added y $x$’s together (and the sum is $y*x$).

Using this table, it is easy to see that at any point, sum == count*x (since count tracks the number of iterations). This is true both before the loop begins and at the end of each iteration, so it will be our loop invariant.

We now add a loop invariant block to our loop:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

val x: Z = Z.read()
val y: Z = Z.read()

var sum: Z = 0
var count: Z = 0

while (count != y) {
    //loop invariant block (still needs to be proved)
    Invariant(
        Modifies(sum, count),
        sum == count * x
    )

    sum = sum + x
    count = count + 1
}

//now sum is x*y

We list sum and count in the Modifies clause because those are the two variables that change value inside the loop.

Proving the loop invariant

In order to prove the correctness of a loop, we must do two things:

Prove the loop invariant is true before the loop begins
Assume the loop invariant is true at the beginning of an iteration, and prove that the invariant is STILL true at the end of the iteration

Proving loop invariant before loop begins

In our multiplication loop above, let’s start by proving the loop invariant before the loop begins. This means that just before the loop, we must prove exactly the claim sum == count*x. We can do this with algebra on the current variable values:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

val x: Z = Z.read()
val y: Z = Z.read()

var sum: Z = 0
var count: Z = 0

//prove the invariant before the loop begins
Deduce(
    1 (     sum == 0        )   by Premise,         //from the "sum = 0" assignment
    2 (     count == 0      )   by Premise,         //from the "count = 0" assignment
    3 (     sum == count*x  )   by Algebra*(1, 2)   //proved EXACTLY the loop invariant
)

while (count != y) {
    Invariant(
        Modifies(sum, count),
        sum == count * x
    )

    sum = sum + x
    count = count + 1

    //we still need to prove the invariant after each iteration
}

//now sum is x*y

Proving loop invariant at the end of each iteration

To prove the loop invariant still holds at the end of an iteration, we must have a logic block at the end of the loop body with exactly the claim in the loop invariant (which will now be referring to the updated values of each variable). Since this step has us assuming the loop invariant is true at the beginning of each iteration, we can list the loop invariant as a premise in a logic block just inside the loop body. Here is the structure we wish to follow for our multiplication loop:

while (count != y) {
    Invariant(
        Modifies(sum, count),
        sum == count * x
    )

    Deduce(
        1 (     sum == count*x      )   by Premise,     //the loop invariant holds
                                                        //at the beginning of an iteration
    )

    sum = sum + x
    count = count + 1

    //need to prove exactly "sum == count*x"
    //to prove our invariant still holds at the end of an iteration
}

We can complete the loop invariant proof by using our tools for processing assignment statements with mutations. Here is the completed verification:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

val x: Z = Z.read()
val y: Z = Z.read()

var sum: Z = 0
var count: Z = 0

//prove the invariant before the loop begins
Deduce(
    1 (     sum == 0        )   by Premise,         //from the "sum = 0" assignment
    2 (     count == 0      )   by Premise,         //from the "count = 0" assignment
    3 (     sum == count*x  )   by Algebra*(1, 2)   //proved EXACTLY the loop invariant
)

while (count != y) {
    Invariant(
        Modifies(sum, count),
        sum == count * x
    )

    Deduce(
        1 (     sum == count*x      )   by Premise,     //the loop invariant holds
                                                        //at the beginning of an iteration
    )

    sum = sum + x

    Deduce(
        1 (     sum == Old(sum) + x     )   by Premise,         //from "sum = sum + x" assignment
        2 (     Old(sum) == count*x     )   by Premise,         //loop invariant WAS true, but sum just changed
        3 (     sum == count*x + x      )   by Algebra*(1,2)    //current knowledge without using Old
    )

    count = count + 1

    Deduce(
        1 (     count == Old(count)+ 1  )   by Premise,         //from "count = count + 1" assignment
        2 (     sum == Old(count)*x + x )   by Premise,         //from previous "sum = count*x + x", 
                                                                //but count has changed
        3 (     sum == (count-1)*x + x  )   by Algebra*(1,2),
        4 (     sum == count*x - x + x  )   by Algebra*(3),
        5 (     sum == count*x          )   by Algebra*(4)      //loop invariant holds at end of iteration
    )
}

//now sum is x*y

Knowledge after loop ends

In the example above, suppose we add the following assert after the loop ends:

assert(sum == x*y)

This seems like a reasonable claim – after all, we said that our loop was supposed to calculated x * y using repeated addition. We have proved the loop invariant, so we can be sure that sum == count*x after the loop…but that’s not quite the same thing. Does count equal y? How do we know?

We can prove our assert statement by considering one more piece of information – if we have exited the loop, we know that the loop condition must be false. In fact, you always know two things (which you can claim as premises) after the loop ends:

The loop condition is false (so we can claim ¬(condition))
The loop invariant is true, since we proved is true at the end of each iteration

We can use those pieces of information to prove our assert statement:

//the multiplication loop example goes here

Deduce(
    1 (     sum == count*x  )   by Premise,     //the loop invariant holds
    2 (     ¬(count != y)   )   by Premise,     //the loop condition is not true
    3 (     count == y      )   by Algebra*(2),
    4 (     sum == x*y      )   by Algebra*1,3  //proves our assert statement
)

assert(sum == x*y)

Functions with loops

If we have a function that includes a loop, we must do the following:

Prove the loop invariant is true before the loop begins
Given that the loop invariant is true at the beginning of an iteration, prove that it is still true at the end of the iteration
Use the combination of the loop invariant and the negation of the loop condition to prove the postcondition

For example, suppose our loop multiplication is inside a function which is tested by some calling code. We would like to add a function contract, our loop invariant proof, and necessary logic blocks to show that our assert holds at the end of the calling code. Here is just the code for the example:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

def mult(x: Z, y: Z) : Z = {
    var sum: Z = 0
    var count: Z = 0

    while (count != y) {
        sum = sum + x
        count = count + 1
    }

    return sum
}

//////////// Test code //////////////

var one: Z = 3
var two: Z = 4

var answer: Z = mult(one, two)
assert(answer == 12)

We start by adding a function contract to mult, which will be the same as our function contract for the recursive version of this function in section 9.2 – y needs to be nonnegative, and we promise to return x*y. Here is the code after adding the function contract and our previous loop verificaton:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

def mult(x: Z, y: Z) : Z = {
    //function contract
    Contract(
        Requires(   y >= 0          ),  //precondition: y should be nonnegative
        Ensures(    Res[Z] == x * y )   //postcondition (we promise to return x*y)
    )

    var sum: Z = 0
    var count: Z = 0

    //prove the invariant before the loop begins
    Deduce(
    1 (     sum == 0        )   by Premise,         //from the "sum = 0" assignment
    2 (     count == 0      )   by Premise,         //from the "count = 0" assignment
    3 (     sum == count*x  )   by Algebra*(1, 2)   //proved EXACTLY the loop invariant
)

    while (count != y) {
        Invariant(
            Modifies(sum, count),
            sum == count * x
        )

        Deduce(
            1 (     sum == count*x      )   by Premise,     //the loop invariant holds
                                                            //at the beginning of an iteration
        )

        sum = sum + x

        Deduce(
            1 (     sum == Old(sum) + x     )   by Premise,         //from "sum = sum + x" assignment
            2 (     Old(sum) == count*x     )   by Premise,         //loop invariant WAS true, but sum just changed
            3 (     sum == count*x + x      )   by Algebra*(1,2)    //current knowledge without using Old
        )

        count = count + 1

        Deduce(
            1 (     count == Old(count)+ 1  )   by Premise,         //from "count = count + 1" assignment
            2 (     sum == Old(count)*x + x )   by Premise,         //from previous "sum = count*x + x", 
                                                                    //but count has changed
            3 (     sum == (count-1)*x + x  )   by Algebra*(1,2),
            4 (     sum == count*x - x + x  )   by Algebra*(3),
            5 (     sum == count*x          )   by Algebra*(4)      //loop invariant holds at end of iteration
        )
    }

    //STILL NEED TO PROVE POSTCONDITION

    return sum
}

//////////// Test code //////////////

var one: Z = 3
var two: Z = 4

//STILL NEED TO ADD VERIFICATION FOR ASSERT

var answer: Z = mult(one, two)
assert(answer == 12)

We can use the negation of the loop condition (¬(count != y)) together with the loop invariant to prove the postcondition will hold before the function returns. We can also apply the same process as in sections 9.1 and 9.2 to prove the precondition in the calling code before calling the mult function, and to use the function’s postcondition after the call to mult to prove our goal assert. Here is the completed example:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._

def mult(x: Z, y: Z) : Z = {
    //function contract
    Contract(
        Requires(   y >= 0          ),  //precondition: y should be nonnegative
        Ensures(    Res[Z] == x * y )   //postcondition (we promise to return x*y)
    )

    var sum: Z = 0
    var count: Z = 0

    //prove the invariant before the loop begins
    Deduce(
    1 (     sum == 0        )   by Premise,         //from the "sum = 0" assignment
    2 (     count == 0      )   by Premise,         //from the "count = 0" assignment
    3 (     sum == count*x  )   by Algebra*(1, 2)   //proved EXACTLY the loop invariant
)

    while (count != y) {
        Invariant(
            Modifies(sum, count),
            sum == count * x
        )

        Deduce(
            1 (     sum == count*x      )   by Premise,     //the loop invariant holds
                                                            //at the beginning of an iteration
        )

        sum = sum + x

        Deduce(
            1 (     sum == Old(sum) + x     )   by Premise,         //from "sum = sum + x" assignment
            2 (     Old(sum) == count*x     )   by Premise,         //loop invariant WAS true, but sum just changed
            3 (     sum == count*x + x      )   by Algebra*(1,2)    //current knowledge without using Old
        )

        count = count + 1

        Deduce(
            1 (     count == Old(count)+ 1  )   by Premise,         //from "count = count + 1" assignment
            2 (     sum == Old(count)*x + x )   by Premise,         //from previous "sum = count*x + x", 
                                                                    //but count has changed
            3 (     sum == (count-1)*x + x  )   by Algebra*(1,2),
            4 (     sum == count*x - x + x  )   by Algebra*(3),
            5 (     sum == count*x          )   by Algebra*(4)      //loop invariant holds at end of iteration
        )
    }

    Deduce(
        1 (     ¬(count != y)       )   by Premise,         //loop condition is now false
        2 (     sum == count*x      )   by Premise,         //loop invariant holds after loop
        3 (     count == y          )   by Algebra*(1),
        4 (     sum == x*y          )   by Algebra*(2,3)    //proves the postcondition
    )

    return sum
}

//////////// Test code //////////////

var one: Z = 3
var two: Z = 4

Deduce(
    1 (     two == 4        )   by Premise,     //from the "two = 4" assignment
    2 (     two >= 0        )   by Algebra*(1)  //proves the mult precondition
)

var answer: Z = mult(one, two)

Deduce(
    1 (     one == 3            )   by Premise,
    2 (     two == 4            )   by Premise,
    3 (     answer == one*two   )   by Premise          //from the mult postcondition
    4 (     answer == 12        )   by Algebra*(1,2,3)  //proves the assert 
)

assert(answer == 12)

How to construct a loop invariant

The most difficult part of the entire process of proving the correctness of a function with a loop is coming up with an appropriate loop invariant. In this section, we will study two additional loops and learn techniques for deriving loop invariants. In general, we need to think about what the loop is doing as it iterates, and what progress it has made so far towards its goal. A good first approach is to trace through the values of variables for several iterations of the loop, as we did with mult above – this helps us identify patterns that can then become the loop invariant.

Example 1: Sum of odds

Suppose n has already been declared and initialized, and that we have this loop:

var total: Z = 0
var i: Z = 0
while (i < n) {
    i = i + 1
    total = total + (2*i - 1)
}

It might be difficult to tell what this code is doing before walking through a few iterations. Let’s make a table showing the values of different variables at different points in the loop:

Variable	Before loop	After iteration 1	After iteration 2	After iteration 3	…	After iteration n
`i`	0	1	2	3	…	n
`total`	$0 $	$1 $	$1 + 3 (= 4)$	$1 + 3 + 5 (= 9)$	…	$1 + 3 + 5 + ... + (2*n-1) (=n^2)$

Now we can see the pattern – we are adding up the first $n$ odd numbers. We can see that at the end of the i-th iteration we have added the first $i$ odd numbers, where $(2*i-1)$ is our most recent odd number. We also see that the sum of the first 1 odd number is 1, the sum of the first 2 odd numbers is $2^2 = 4$, …, and the sum of the first $n$ odd numbers is $n^2$.

Since our loop invariant should describe what progress it has made towards its goal of adding the first $n$ odd numbers, we can see that the loop invariant should be that at any point (before the loop begins and at the end each iteration), $total$ holds the sum of the first $i$ numbers (whose value is $i^2$). We first try this as our loop invariant:

var total: Z = 0
var i: Z = 0
while (i < n) {
    Invariant(
        Modifies(i, n),
        total == i*i
    )

    i = i + 1
    total = total + (2*i - 1)
}

Another consideration of writing a loop invariant is that we should be able to deduce our overall goal once the loop ends. After our loop, we want to be sure that total holds the sum of the first n odd numbers – i.e., that total == n*n. Our loop invariant tells us that total == i*i after the loop ends – but does n necessarily equal i?

The way it is written, we can’t be certain. We do know that the loop condition must be false after the loop, or that ¬(i < n). But this is equivalent to i >= n and not i == n. We need to tighten our invariant to add a restriction that i always be less than or equal to n:

var total: Z = 0
var i: Z = 0
while (i < n) {
    Invariant(
        Modifies(i, n),
        total == i*i,
        i <= n
    )
    
    i = i + 1
    total = total + (2*i - 1)
}

After the loop ends, we can now combine the negation of the loop condition, ¬(i < n) together with the i <= n portion of the invariant to deduce that i == n. Together with the other half of the invariant – total == i*i – we can be sure that total == n*n when the loop ends.

Example 2: factorial

Suppose n has already been declared and initialized, and that we have this loop:

var prod: Z = 1
var i: Z = 1
while (i != n) {
    i = i + 1
    prod = prod * i
}

As before, let’s make a table showing the values of different variables at different points in the loop:

Variable	Before loop	After iteration 1	After iteration 2	…	After iteration n
`i`	1	2	3	…	n
`prod`	$1 $	$1 * 2$	$1 * 2 * 3$	…	$1 * 2 * 3 * ... * n$

From this table, we can clearly see that after $i$ iterations, $prod == i!$ (i factorial). This should be our loop invariant…but as with many other languages, Logika does not recognize ! as a factorial operator (instead, it is a negation operator). In the next section, we will see how to create a Logika fact to help define the factorial operation. We will then be able to use that Logika fact in place of ! to let our invariant be a formalization of: prod equals i factorial.

Logika Facts

We saw at the end of section 9.3 that we sometimes need a more expressive way of specifying a loop invariant (or, similarly, for postconditions). In our last example, we wanted to describe the factorial operation. We know that $n! = n * (n-1) * (n-2) * ... * 2 * 1$, but we don’t have a way to describe the “…” portion using our current tools.

In this section, we introduce Logika facts, which will let us create our own recursive proof functions that we can use in invariants and postconditions. We will usually want to use a Logika fact anytime our invariant or postcondition needs to express something that has a “…” to demonstrate a pattern.

Logika fact syntax

Logika allows these proof functions to be written in multiple ways, but we will start with the most straightforward of these options:

@spec def proofFunction(paramList): returnType = $

@spec def proofFacts = Fact(
    proofFunction(baseCase) == baseValue,
    ...
    ∀( (x: Z) => (rangeOfX) → (proofFunction(x) == proofFunction(x - 1) * x) )
)

In the above definition, proofFunction is the name we give our proof function, paramList is the list of parameter names and types needed for this proof function (which are formatted exactly like a parameter list in a regular Logika function), and returnType is the return type of the proof function (usually either Z for integer or B for boolean). The = $ at the end of the proof function is indicating that its definition will be provided later.

Below the proof function, we include the proof facts, which is a recursive definition of the values for our proof function. We include one or more base cases, which list the value of our proof function for its smallest possible input (or for the smallest several inputs). Finally, we include our recursive case as a quantified statement – it lists the value of our proof function on all inputs bigger than our base cases. This recursive case uses the proof function’s definition for a smaller value, like proofFunction(x-1).

Logika facts are defined at the top of the Logika file, below the imports but before any of the code.

Example: Logika fact to define factorial

It is much easier to see how Logika facts work by using an example. Suppose we want to define the factorial operation. The first step is to come up with a recursive definition, which has us defining the operation the same way we would in a recursive function – with one or more base cases where we can define the operation for the simplest case, and one or more recursive cases that express a general instance of the problem in terms of a smaller instance.

For factorial, the simplest version is $1!$, which is just 1. In the general case, we have that:

$$ n! = n * (n-1) * (n-2) * ... * 2 * 1 = n * (n-1)! $$

So we can write the following recursive definition:

Base case: $1! = 1$
Recursive case: for values of $n$ greater than 1, $n! = n * (n-1)!$

And we can then translate the recursive definition to a Logika fact:

@spec def factFunction(n: Z): Z = $

@spec def factorialFacts = Fact(
    factFunction(1) == 1,
    ∀ ( (x: Z) => (x > 1) → (factFunction(x) == factFunction(x-1)*x) )
)

Let’s consider each portion of this proof function. Here, factDef is the name given to the proof function. It takes one parameter, n, which is an integer, and it returns an integer. We have two possible ways of calculating the value for the proof function, which we detail in factorialFacts. First, we define our base case:

factFunction(1) == 1

Which says that factFunction(n) is 1 if $n == 1$. This is the same as our base case in our recursive definition for factorial – $1! = 1$.

Next, consider the recursive case of our proof function:

∀ ( (x: Z) => (x > 1) → (factFunction(x) == factFunction(x-1)*x) )

This case states that for all integers x that are bigger than 1, we define factFunction(x) == x * factFunction(x - 1). This is the same as our recursive case in our recursive definition for factorial – for values of $n$ greater than 1, $n! = n * (n-1)!$.

Evaluating a Logika fact

Suppose we used our factorialFacts proof function to calculate factFunction(3). We would have:

factFunction(3) == 3 * factFunction(2)      //we use the recursive case, since 3 > 1
factFunction(2) == 2 * factFunction(1)      //we use the recursive case, since 2 > 1
factFunction(1) == 1                        //we use the base case

Once we work down to:

factFunction(1) == 1

We can plug 1 in for facfactFunctiontDef(1) in factFunction(2) == 2 * factFunction(1), which gives us:

factFunction(2) == 2

Similarly, we can plug 2 in for factFunction(2) in factFunction(3) == 3 * factFunction(2), and see that:

factFunction(3) == 6

Using Logika facts as justifications

If we had our proof function, factFunction, then we could pull its two facts from its factorialFacts recursive definition into a proof block like this:

Deduce(
    1 (     factFunction(1) == 1                                                )   by ClaimOf(factorialFacts _),                                             
    2 (     ∀ ( (x: Z) => (x > 1) → (factFunction(x) == factFunction(x-1)*x) )  )   by ClaimOf(factorialFacts _)
)

Note that we must pull in the definitions EXACTLY as they are written in the proof function. The justification is always ClaimOf(proofFacts _) where proofFacts is the name of the recursive definition.

Using Logika facts in postconditions and invariants

Consider the following full Logika program that includes a function to find and return a factorial, as well as test code that calls our factorial function:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
import org.sireum.justification.natded.pred._

// n! = n * (n-1) * (n-2) * .. * 1
// 1! = 1
def factorial(n: Z): Z = {
    var i: Z = 1        //how many multiplications we have done
    var product: Z = 1  //our current calculation

    while (i != n) {
        i = i + 1
        product = product * i
    }

    return product
}

//////// Test code ///////////

var num: Z = 2

var answer: Z = factorial(num)

assert(answer == 2)

We want to add a function contract, loop invariant block, and supporting logic blocks to demonstrate that factorial is returning n! and to prove the assert in our text code.

Writing a function contract using a Logika fact

We want our factorial function contract to say that it is returning n!, and that it is only defined for values of n that are greater than or equal to 0. We recall that our Logika fact, factFunction, defines the factorial operation:

@spec def factFunction(n: Z): Z = $

@spec def factorialFacts = Fact(
    factFunction(1) == 1,
    ∀ ( (x: Z) => (x > 1) → (factFunction(x) == factFunction(x-1)*x) )
)

And we will use factFunction to define what we mean by “factorial” in our factorial function contract:

def factorial(n: Z): Z = {
    Contract(
        Requires(   n >= 1                      ),  //factFunction(n) is only defined when n >= 1
        Ensures(    Res[Z] == factFunction(n)   )   //we promise to return factFunction(n), where factFunction defines n!
    )

    //code for factorial function
}

Writing a loop invariant block using a Logika fact

We can similarly use factFunction in our loop invariant block. We noted at the end of section 9.3 that the invariant in our loop should be: prod equals i factorial. Now we have a way to express what we mean by “factorial”, so our invariant will be: prod == factFunction(i). Since the factFunction proof function is only defined for parameters greater than or equal to 1, we need to add a second piece to the invariant to guarantee that i will always be greater than or equal to 1. We now have the following loop invariant block:

while (i != n) {
    Invariant(
        Modifies(i, product),
        product == factFunction(i),
        i >= 1
    )

    //loop body
}

Finishing the verification

All that remains is to:

Prove our loop invariant holds before the loop begins
When we assume the loop invariant holds at the beginning of an iteration, prove that it still holds at the end of the iteration
Use the loop invariant together with the negation of the loop condition to prove the factorial postcondition
Prove the precondition holds in the calling code just before calling factorial
Use the postcondition after calling factorial to prove the final assert

Here is the completed verification:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
import org.sireum.justification.natded.pred._

@spec def factFunction(n: Z): Z = $

@spec def factorialFacts = Fact(
    factFunction(1) == 1,
    ∀((x: Z) => (x > 1) → (factFunction(x) == factFunction(x-1)*x))
)


def factorial(n: Z): Z = {
    Contract(
        Requires(   n >= 1                      ),  //factFunction(n) is only defined when n >= 1
        Ensures(    Res[Z] == factFunction(n)   )   //we promise to return factFunction(n), where factFunction defines n!
    )

    var i: Z = 1        //how many multiplications we have done
    var product: Z = 1  //my current calculation

    //Prove invariant before loop begins
    Deduce(
        1 (     i == 1                      ) by Premise,
        2 (     product == 1                ) by Premise,

         //pull in proof function base case
        3 (     factFunction(1) == 1        ) by ClaimOf(factorialFacts _),

        //proves first loop invariant holds 
        4 (     product == factFunction(i)  ) by Algebra*(1, 2, 3),

        //proves second loop invariant holds 
        5 (     i >= 1                      ) by Algebra*(1)
    )

    while (i != n) {
        Invariant(
            Modifies(i, product),
            product == factFunction(i),
            i >= 1
        )

        i = i + 1

        Deduce(
            //from "i = i + 1"
            1 (     i == Old(i) + 1                  ) by Premise,

            //loop invariant held before changing i
            2 (     product == factFunction(Old(i))  ) by Premise,

            //rewrite invariant with no "Old"
            3 (     product == factFunction(i - 1)   ) by Algebra*(1, 2),

            //second loop invariant held before changing i
            4 (     Old(i) >= 1                      ) by Premise,

            //needed for the Logika fact
            5 (     i > 1                            ) by Algebra*(1, 4)
        )

        product = product * i

        //Prove invariant still holds at end of iteration
        Deduce(
            //from "product = product * i"
            1 (  product == Old(product) * i                                        ) by Premise,

            //from previous logic block
            2 (  Old(product) == factFunction(i - 1)                                ) by Premise,

             //pull in recursive case from proof function
            3 (  ∀( (x: Z) => x > 1 → factFunction(x) == factFunction(x - 1) * x )  ) by ClaimOf(factorialFacts _),

            //plug in "i" for "x" (where i is of type Z)
            4 (  i > 1 → factFunction(i) == factFunction(i - 1) * i                 ) by AllE[Z](3),

            //from previous logic block
            5 (  i > 1                                                              ) by Premise,

            //i > 1, so get right side of →
            6 (  factFunction(i) == factFunction(i - 1) * i                         ) by ImplyE(4, 5),
            7 (  product == factFunction(i - 1) * i                                 ) by Algebra*(1, 2),

            //proves first invariant still holds
            8 (  product == factFunction(i)                                         ) by Algebra*(6, 7),

            //proves second invariant still holds
            9 (  i >= 1                                                             ) by Algebra*(5)
        )
    }

    //Prove postcondition
    Deduce(
        1 (     product == factFunction(i)  ) by Premise,      //loop invariant
        2 (     !(i != n)                   ) by Premise,      //loop condition false
        3 (     i == n                      ) by Algebra*(2),
        4 (     product == factFunction(n)  ) by Algebra*(1, 3)
    )

    return product
}

//////// Test code ///////////

var num: Z = 2

//Prove precondition
Deduce(
    1 (     num == 2  ) by Premise,
    2 (     num >= 1  ) by Algebra*(1)     //proves factorial precondition
)

var answer: Z = factorial(num)

Deduce(
    1 (  answer == factFunction(num)                                        ) by Premise,       //factorial postcondition
    2 (  num == 2                                                           ) by Premise,
    3 (  answer == factFunction(2)                                          ) by Algebra*(1, 2),

    //pull in recursive case from proof function
    4 (  ∀( (x: Z) => x > 1 → factFunction(x) == factFunction(x - 1) * x )  ) by ClaimOf(factorialFacts _),

     //plug in "2" for "x" (where 2 is an integer of type Z)
    5 (  2 > 1 → factFunction(2) == factFunction(2 - 1) * 2                 ) by AllE[Z](4),
    6 (  2 > 1                                                              ) by Algebra*(),

    //2 > 1, so use →
    7 (  factFunction(2) == factFunction(2 - 1) * 2                         ) by ImplyE(5, 6),

    //pull in base case from proof function
    8 (  factFunction(1) == 1                                               ) by ClaimOf(factorialFacts _),
    9 (  factFunction(2) == factFunction(1) * 2                             ) by Algebra*(7),
    10 (  factFunction(2) == 2                                              ) by Algebra*(8, 9),

    //proves claim in assert
    11 (  answer == 2                                                       ) by Algebra*(1, 2, 10)
)

assert(answer == 2)

Logika fact for multiplication

Suppose we wanted to create a Logika fact that recursively defined multiplication. We first recursively define how we would multiply $x * y$. We know that our base case will be when $y == 0$, because anything times 0 is 0. We also saw that multiplication can be defined as repeated addition, so that $x * y == x + x + ... x$ for a total of $y$ additions. We also see that $x * y == x + x * (y-1)$, since we can pull out one of the additions and then have $y-1$ additions left to do.

Here is our recursive definition of the problem:

Base case: for all numbers x, x * 0 is 0
Recursive case: for all numbers x and all positive numbers y, x * y = x + x * (y-1)

We can translate this directly to a proof function:

@spec def multFunction(m: Z, n: Z): Z = $

@spec def multFacts = Fact(
    //anything multiplied by 0 is just 0
    ∀((x: Z) => multFunction(x, 0) == 0 ),

    //defines m * n = m + m + ... + m (n times)
    ∀( (x: Z) => ∀( (y: Z) => (y > 1) → (multFunction(x, y) == multFunction(x,y-1)) ) )
)

We could use this Logika fact in the postcondition and loop invariant block for a multiplication function as follows:

// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
import org.sireum.justification.natded.pred._

@spec def multFunction(m: Z, n: Z): Z = $

@spec def multFacts = Fact(
    //anything multiplied by 0 is just 0
    ∀((x: Z) => multFunction(x, 0) == 0 ),

    //defines m * n = m + m + ... + m (n times)
    ∀( (x: Z) => ∀( (y: Z) => (y > 1) → (multFunction(x, y) == multFunction(x,y-1)) ) )
)


//want to find: num1 + num1 + ... + num1 (a total of num2 times)
def mult(num1: Z, num2: Z): Z = {
    Contract( 
        Requires( num2 >= 1 ),
        Ensures( Res[Z] == multFunction(num1, num2) )
    )
  
    var answer: Z = 0
    var cur: Z = 0

    while (cur != num2) {
        Invariant(
            Modifies(cur, answer),
            answer == multFunction(num1, cur),
            cur >= 0
        )

        cur = cur + 1
        answer = answer + num1
    }

    return answer
}

The example above does not include the verification steps to prove the loop invariant and postcondition, but those things could be accomplished in the same way as for the factorial function.

Logika fact for Fibonacci numbers

The Fibonacci sequence is:

$$ 1, 1, 2, 3, 5, 8, 13, ... $$

The first two Fibonacci numbers are both 1, and subsequent Fibonacci numbers are found by adding the two previous values. In the sequence above, we see that the two latest numbers were 8 and 13, so the next number in the sequence will be $8 + 13 = 21$.

We can recursively define the Fibonacci sequence as follows:

Base case 1: the first Fibonacci number is 1
Base case 2: the second Fibonacci number is 1
Recursive case: for all numbers x greater than 2, the x-th Fibonacci number is the (x-1)-th Fibonacci number + the (x-2)-th Fibonacci number

We can translate this directly to a Logika fact:

//defines the nth number in the Fibonacci sequence
//1, 1, 2, 3, 5, 8, 13, ...
@spec def fibFunction(n: Z): Z = $

@spec def fibFacts = Fact(
    fibFunction(1) == 1,
    fibFunction(2) == 2,
    ∀( (x: Z) => (x > 2) → fibFunction(x-1) + fibFunction(x-2) )

    //defines m * n = m + m + ... + m (n times)
    ∀( (x: Z) => ∀( (y: Z) => (y > 1) → (multFunction(x, y) == multFunction(x,y-1)) ) )
)

Which we could use in a postcondition and loop invariant if we wrote a function to compute the Fibonacci numbers.

Summary

Chapter 9 showed us how to write function contracts to specify the requirements and behavior of functions, and loop invariants to reason about the behavior and progress of loops. To wrap up, we briefly summarize the process for verifying a program that includes one or more functions with loops:

Step 1: Write function contracts

Write a function contract for any function that doesn’t already have one. Function contracts go just inside the function defintion, and look like:

Contract(
    Requires( preconditions ),
    Ensures( postconditions )
)

Here, preconditions is a comma-separated list of any requirements your function has about the range of its parameters, and postconditions is a comma-separated list describing the impact of calling the function (in this chapter, the postcondition always describes how the return value relates to the parameters.) If you’re not sure what to write as the postcondition, try walking through your function with different parameters to get a sense for the pattern of what the function is doing in relation to the parameters. If you were given a Logika proof function, you will likely need to use it in the postcondition (and loop invariant) to describe the behavior.

Step 2: Write loop invariant blocks

Write a loop invariant block for any loop that doesn’t already have one. Loop invariant blocks go just inside the loop (before any code) and look like:

Invariant(
    Modifies(comma-separated list of variables),
    Invariant_1,
    Invariant_2,
    ...
)

Each Invariant_i describes an invariant for the loop, which should describe the progress the loop has made toward its goal (the loop invariant will often greatly resemble the postcondition for the enclosing function). Loop invariants occasionally need to specify the range of different variables, especially if the invariant uses Logika facts (which may only be defined for particular values) or if you need more information about the final value of a variable when a loop terminates. I recommend making a table of variable values for several iterations of your loop to get a sense of the relationship between variables – this relationship is what will become the loop invariant.

The Modifies clause lists all variables that are modified in the loop body.

Step 3: Prove invariant holds before loop begins

In each loop, prove your invariant holds before the loop begins. You may need to pull in the function’s precondition as a premise in this step. You must prove EXACTLY the claim in all pieces of the loop invariant. If your loop invariant involves a Logika fact, you may need to pull in a piece of the fact definition to help prove the invariant.

Step 4: Prove invariant still holds at end of iteration

In each loop, prove your invariant still holds at the end of each iteration. Start by pulling in each part of the loop invariant as a premise before the loop body begins. Use logic blocks to process each statement in the body of the loop. By the end of the loop, you must prove EXACTLY the claim in all pieces of the loop invariant. (Again, if your loop invariant involves a Logika fact, you’ll want to pull in a piece of the fact definition to help with this step.)

Step 5: Prove the postcondition

Use the combination of the loop invariant and the negation of the loop condition to prove the postcondition just before your function ends.

Step 6: Prove the precondition before each function call

Before any function call, prove exactly the precondition(s) for the function (using whatever values you are passing as parameters).

Step 7: Use postcondition after each function call

After returning from each function call, pull the function’s postcondition into a logic block as a premise (using whatever values you passed as parameters). Use this information to help prove any asserts.