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.
Subsections of Functions and Loops
Functions
A function in Logika 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 Logika:
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 expressionWhere 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:
l"""{
requires (preconditions)
modifies (variable list)
ensures (postconditions)
}"""Here is a summary of the different function contract clauses:
requires: lists the preconditions for the function. We can also use the keywordpreinstead ofrequires. If there are no preconditions, we can skip this clause. If we have multiple preconditions, we can list them on separate lines (where subsequent lines are tabbed over underrequires).modifies: lists the name of any sequence parameters and/or global variables that are modified by the function. We can skip this clause until chapter 10, when we will see sequences and global variables.ensures: lists the postconditions for the function. We can also use the keywordpostinstead ofensures. If we have multiple postconditions, we can list them on separate lines (where subsequent lines are tabbed over underensures).
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 = {
l"""{
requires b != 0
...
}"""
val ans: Z = a/b
return ans
}Logika will throw 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 logic block just after the function contract:
def example(a: Z, b: Z) : Z = {
l"""{
requires precondition1
precondition2
...
...
}"""
//we can list the preconditions as premises
l"""{
1. precondition1 premise
2. precondition2 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 can use the keyword
resultto refer to the object returned by the function (we will only use this keyword in the function contract). -
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 = {
l"""{
requires b != 0
ensures result == a/b
}"""
val ans: Z = a/b
return ans
}In order to prove a postcondition involving the return value, we must have logic blocks just before returning that demonstrate each postcondition claim, using the variable name being returned instead of the result 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 = {
l"""{
requires b != 0
ensures result == a/b
}"""
val ans: Z = a/b
l"""{
1. b != 0 premise //precondition (needed for division)
2. ans == a/b premise //satisfies the postcondition
//(from the "ans = a/b" assignment)
}"""
return ans
}Logika will throw 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).
Below, we will see the syntax for the verification of code that calls a function. We will refer to our finished div function:
def div(a: Z, b: Z) : Z = {
l"""{
requires b != 0
ensures result == a/b
}"""
val ans: Z = a/b
l"""{
1. b != 0 premise //precondition (needed for division)
2. ans == a/b premise //satisfies the postcondition
//(from the "ans = a/b" assignment)
}"""
return ans
}The “calling code” in Logika goes outside of any function definition. Typically, I place the calling code at the bottom of the Logika file, after all functions. Recall that this is the code executed first by Logika, 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 Logika 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 logic 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
l"""{
1. x == 10 premise //from the "x = 10" assignment
2. y == 2 premise //from the "y = 2" assignment
3. y != 0 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
l"""{
1. x == 10 premise //from the "x = 10" assignment
2. y == 2 premise //from the "y = 2" assignment
3. y != 0 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
l"""{
1. x == 10 premise //from the "x = 10" assignment
2. y == 2 premise //from the "y = 2" assignment
3. y+1 != 0 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 result, then the calling code can list exactly that postcondition using whatever variable it used to store the return value in place of result and using whatever values were passed in place of the parameter names. In the div example above where we divde 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
l"""{
1. x == 10 premise //from the "x = 10" assignment
2. y == 2 premise //from the "y = 2" assignment
3. y+1 != 0 algebra 2 //Satisfies the precondition for our second parameter (y+1)
}"""
val num: Z = div(x-1, y+1)
l"""{
1. num == (x-1)/(y+1) 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 logic block, plugging in the values for x and y and doing some algebra:
val x: Z = 10
val y: Z = 2
l"""{
1. x == 10 premise //from the "x = 10" assignment
2. y == 2 premise //from the "y = 2" assignment
3. y+1 != 0 algebra 2 //Satisfies the precondition for our second parameter (y+1)
}"""
val num: Z = div(x-1, y+1)
l"""{
1. num == (x-1)/(y+1) premise //postcondition of div
2. x == 10 premise //x is unchanged from the "x = 10" assignment
3. y == 2 premise //y is unchanged from the "y = 2" assignment
4. num == 9/3 algebra 1 2 3
5. num == 3 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:
import org.sireum.logika._
def plusOne(n: Z): Z = {
l"""{
requires n >= 0 //precondition: parameter should be non-negative
ensures result == n+1 //postcondition 1: we promise returned value is one more than parameter
result > 0 //postcondition 2: we promise returned value is greater than 0
}"""
val answer: Z = n+1
l"""{
1. n >= 0 premise //from the precondition
2. answer == n+1 premise //from the "answer = n+1" assignment
//proves the first postcondition
3. answer > 0 algebra 1 2 //proves the second postcondition
}"""
return answer
}
////////// Test code ///////////////
var x: Z = 5
l"""{
1. x == 5 premise //from the "x=5" assignment
2. x >= 0 algebra 1 //proves the plusOne precondition
}"""
var added: Z = plusOne(x)
l"""{
//I can list the postcondition (what is returned) as a premise
1. x == 5 premise //x is unchanged
2. added == x+1 premise //plusOne postcondition 1
3. added > 0 premise //plusOne postcondition 2
4. added == 6 algebra 1 2
5. added == 6 ∧ added > 0 ^i 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:
import org.sireum.logika._
//find the max between x and y
def findMax(x: Z, y: Z): Z = {
l"""{
//no precondition needed
ensures
result >= x //postcondition 1
result >= y //postcondition 2
result == x v result == y //postcondition 3
}"""
var max: Z = 0
l"""{
1. max == 0 premise
}"""
if (x > y) {
l"""{
1. max == 0 premise
2. x > y premise //IF condition is true
}"""
max = x
l"""{
1. max == x premise
2. max >= x algebra 1
3. x > y premise
4. max >= y algebra 1 3
}"""
} else {
l"""{
1. max == 0 premise
2. ¬(x > y) premise //IF condition is not true
3. x <= y algebra 2
}"""
max = y
l"""{
1. max == y premise
2. x <= y premise
3. max >= x algebra 1 2
4. max >= y algebra 1
}"""
}
//prove the postconditions
l"""{
//true in both the if and the else
1. max >= x premise //proves postcondition 1
2. max >= y premise //proves postcondition 2
//first was true in if, second true in else
3. max == x v max == y 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)
l"""{
1. biggest >= num1 premise //findMax postcondition 1
2. biggest >= num2 premise //findMax postcondition 2
3. biggest == num1 v biggest == num2 premise //findMax postcondition 3
//pull in the initial values
4. num1 == 3 premise
5. num2 == 2 premise
6. biggest >= 3 algebra 1 4
7. biggest >= 2 algebra 2 5
8. biggest == 3 v biggest == num2 subst1 4 3
9. biggest == 3 v biggest == 2 subst1 5 8
//OR-elimination
10. {
11. biggest == 3 assume
}
12. {
13. biggest == 2 assume
14. ¬(biggest >= 3) algebra 13
15. ⊥ ¬e 6 14
16. biggest == 3 ⊥e 15
}
17. biggest == 3 ve 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
yis 0, we have no work to do. Adding together 0x’s is just 0. - Recursive case: if
yis bigger than 0, we do ONE addition (x + ...) and recursively add the remainingy - 1numbers. (This will become our recursive call.)
With those cases in mind, we can write a recursive mult function:
import org.sireum.logika._
def mult(x: Z, y: Z): Z = {
var ans: Z = 0
if (y > 0) {
var addRest: Z = mult(x, y-1)
ans = x + addRest
} else {
//do nothing
}
return ans
}Note that we separated the recursive call (def addRest: Z = mult(x, y-1)) from adding on the next piece (ans = x + addRest). In 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)
addRest = mult(4, 1) => mult(4, 1)
ans = 4 + addRest (x = 4, y = 1)
returns ans addRest = mult(4, 0) => mult(4, 0)
ans = 4 + addRest (x = 4, y = 0)
returns ans ans = 0
returns 0We 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)
addRest = mult(4, 0) = 0
ans = 4 + addRest = 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)
addRest = mult(4, 1) = 4
ans = 4 + addRest = 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 result == x*y). Here is the function with the function contract:
import org.sireum.logika._
def mult(x: Z, y: Z): Z = {
//we still need to add the verification logic blocks
l"""{
requires y >= 0
ensures result == x*y
}"""
var ans: Z = 0
if (y > 0) {
var addRest: Z = mult(x, y-1)
ans = x + addRest
} 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:
var addRest: Z = 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:
import org.sireum.logika._
def mult(x: Z, y: Z): Z = {
//we still need to prove the postcondition
l"""{
requires y >= 0
ensures result == x*y
}"""
var ans: Z = 0
if (y > 0) {
l"""{
1. y > 0 premise //IF condition is true
2. y-1 >= 0 algebra 1 //Proves the precondition for the recursive call
}"""
var addRest: Z = mult(x, y-1)
ans = x + addRest
} 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 addRest: Z = mult(x, y-1), we know that addRest == x*(y-1) (the first parameter, x, times the second parameter, y-1). Here is the completed verification
import org.sireum.logika._
def mult(x: Z, y: Z): Z = {
//verification complete!
l"""{
requires y >= 0
ensures result == x*y
}"""
var ans: Z = 0
if (y > 0) {
l"""{
1. y > 0 premise //IF condition is true
2. y-1 >= 0 algebra 1 //Proves the precondition for the recursive call
}"""
var addRest: Z = mult(x, y-1)
l"""{
1. addRest == x*(y-1) premise //Postcondition from the recursive call
2. addRest == x*y - x algebra 1
}"""
ans = x + addRest
l"""{
1. addRest == x*y - x premise //Pulled from previous block
2. ans == x + addRest premise //From the "ans = x + addRest" assignment statement
3. ans == x + x*y - x algebra 1 2
4. ans == x*y 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
l"""{
1. ¬(y > 0) premise //if condition is false
2. y >= 0 premise //precondition
3. y == 0 algebra 1 2
4. ans == 0 premise //ans is unchanged
5. ans == x*y algebra 3 4 //Showed the postcondition for the ELSE branch
}"""
}
//Tie together what we learned in both branches
l"""{
1. ans == x*y 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:
l"""{
1. 2 >= 0 algebra //proves the precondition
}"""
val times: Z = mult(4, 2)
l"""{
1. times == 4*2 premise //mult postcondition
2. times == 8 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 Logika 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 use a logic block to indicate our loop invariant. This loop invariant block will go just inside the loop, before the loop body:
while (condition) {
l"""{
invariant (expression(s))
modifies (variable list)
}"""
//loop body
}Here is a summary of the different loop invariant clauses:
invariant: lists the invariant for the function. If we have multiple invariants, we can list them on separate lines (where subsequent lines are tabbed over underinvariant).modifies: lists the name of any variables that are modified in the loop body.
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):
import org.sireum.logika._
val x: Z = readInt()
val y: Z = readInt()
var sum: Z = 0
var count: Z = 0
while (count != y) {
sum = sum + x
count = count + 1
}
//now sum is x*yBefore 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:
import org.sireum.logika._
val x: Z = readInt()
val y: Z = readInt()
var sum: Z = 0
var count: Z = 0
while (count != y) {
//loop invariant block (still needs to be proved)
l"""{
invariant sum == count*x
modifies sum, count
}"""
sum = sum + x
count = count + 1
}
//now sum is x*yWe 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:
import org.sireum.logika._
val x: Z = readInt()
val y: Z = readInt()
var sum: Z = 0
var count: Z = 0
//prove the invariant before the loop begins
l"""{
1. sum == 0 premise //from the "sum = 0" assignment
2. count == 0 premise //from the "count = 0" assignment
3. sum == count*x algebra 1 2 //proved EXACTLY the loop invariant
}"""
while (count != y) {
l"""{
invariant sum == count*x
modifies sum, count
}"""
sum = sum + x
count = count + 1
//we still need to prove the invariant after each iteration
}
//now sum is x*yProving 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) {
l"""{
invariant sum == count*x
modifies sum, count
}"""
l"""{
1. sum == count*x 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:
import org.sireum.logika._
val x: Z = readInt()
val y: Z = readInt()
var sum: Z = 0
var count: Z = 0
//prove the invariant before the loop begins
l"""{
1. sum == 0 premise //from the "sum = 0" assignment
2. count == 0 premise //from the "count = 0" assignment
3. sum == count*x algebra 1 2 //proved EXACTLY the loop invariant
}"""
while (count != y) {
l"""{
invariant sum == count*x
modifies sum, count
}"""
l"""{
1. sum == count*x premise //the loop invariant holds
//at the beginning of an iteration
}"""
sum = sum + x
l"""{
1. sum == sum_old + x premise //from "sum = sum + x" assignment
2. sum_old == count*x premise //loop invariant WAS true, but sum just changed
3. sum == count*x + x algebra 1 2 //current knowledge without using _old
}"""
count = count + 1
l"""{
1. count == count_old + 1 premise //from "count = count + 1" assignment
2. sum == count_old*x + x premise //from previous "sum = count*x + x",
//but count has changed
3. sum == (count-1)*x + x algebra 1 2
4. sum == count*x - x + x algebra 3
5. sum == count*x algebra 4 //loop invariant holds at end of iteration
}"""
}
//now sum is x*yKnowledge 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
l"""{
1. sum == count*x premise //the loop invariant holds
2. ¬(count != y) premise //the loop condition is not true
3. count == y algebra 2
4. sum == x*y 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:
import org.sireum.logika._
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:
import org.sireum.logika._
def mult(x: Z, y: Z) : Z = {
//function contract
l"""{
requires y >= 0 //precondition: y should be nonnegative
ensures result == x*y //postcondition (we promise to return x*y)
}"""
var sum: Z = 0
var count: Z = 0
//prove the invariant before the loop begins
l"""{
1. sum == 0 premise //from the "sum = 0" assignment
2. count == 0 premise //from the "count = 0" assignment
3. sum == count*x algebra 1 2 //proved EXACTLY the loop invariant
}"""
while (count != y) {
l"""{
invariant sum == count*x
modifies sum, count
}"""
l"""{
1. sum == count*x premise //the loop invariant holds
//at the beginning of an iteration
}"""
sum = sum + x
l"""{
1. sum == sum_old + x premise //from "sum = sum + x" assignment
2. sum_old == count*x premise //loop invariant WAS true, but sum just changed
3. sum == count*x + x algebra 1 2 //current knowledge without using _old
}"""
count = count + 1
l"""{
1. count == count_old + 1 premise //from "count = count + 1" assignment
2. sum == count_old*x + x premise //from previous "sum = count*x + x",
//but count has changed
3. sum == (count-1)*x + x algebra 1 2
4. sum == count*x - x + x algebra 3
5. sum == count*x 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:
import org.sireum.logika._
def mult(x: Z, y: Z) : Z = {
//function contract
l"""{
requires y >= 0 //precondition: y should be nonnegative
ensures result == x*y //postcondition (we promise to return x*y)
}"""
var sum: Z = 0
var count: Z = 0
//prove the invariant before the loop begins
l"""{
1. sum == 0 premise //from the "sum = 0" assignment
2. count == 0 premise //from the "count = 0" assignment
3. sum == count*x algebra 1 2 //proves EXACTLY the loop invariant
}"""
while (count != y) {
l"""{
invariant sum == count*x
modifies sum, count
}"""
l"""{
1. sum == count*x premise //the loop invariant holds
//at the beginning of an iteration
}"""
sum = sum + x
l"""{
1. sum == sum_old + x premise //from "sum = sum + x" assignment
2. sum_old == count*x premise //loop invariant WAS true, but sum just changed
3. sum == count*x + x algebra 1 2 //current knowledge without using _old
}"""
count = count + 1
l"""{
1. count == count_old + 1 premise //from "count = count + 1" assignment
2. sum == count_old*x + x premise //from previous "sum = count*x + x",
//but count has changed
3. sum == (count-1)*x + x algebra 1 2
4. sum == count*x - x + x algebra 3
5. sum == count*x algebra 4 //proves loop invariant holds at end of iteration
}"""
}
l"""{
1. ¬(count != y) premise //loop condition is now false
2. sum == count*x premise //loop invariant holds after loop
3. count == y algebra 1
4. sum == x*y algebra 2 3 //proves the postcondition
}"""
return sum
}
//////////// Test code //////////////
var one: Z = 3
var two: Z = 4
l"""{
1. two == 4 premise //from the "two = 4" assignment
2. two >= 0 algebra 1 //proves the mult precondition
}"""
var answer: Z = mult(one, two)
l"""{
1. one == 3 premise
2. two == 4 premise
3. answer == one*two premise //from the mult postcondition
4. answer == 12 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) {
l"""{
invariant total == i*i
modifies i, n
}"""
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) {
l"""{
invariant total == i*i
i <= n
modifies 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:
l"""{
fact
def proofFunctionName(paramList) : returnType
factName1. //describe when proofFunctionName has its first possible value
...
factNameN. //describe when proofFunctionName has its last possible value
}"""In the proof function definition, proofFunctionName 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).
Below the proof function definition, we include a line for each possible way to calculate its value. Usually, at least one of the lines includes a recursive defintion – relating the value of something like proofFunctionName(n) to the proof function’s definition for a smaller value, like proofFunctionName(n-1). The label, such as factNameN, names the proof rule. We will be able to pull in a particular line of the definition into a logic block by using the justification fact factNameN.
Logika facts are defined at the top of the Logika file, below the import 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:
l"""{
fact
def factDef(n: Z): Z
fOne. factDef(1) == 1
fBig. ∀x: Z x > 1 → factDef(x) == x * factDef(x - 1)
}"""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. First, we define fOne:
fOne. factDef(1) == 1fOne defines factDef(1) as 1; i.e., factDef(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 definition for fBig:
fBig. ∀x: Z x > 1 → factDef(x) == x * factDef(x - 1)fBig states that for all integers x that are bigger than 1, we define factDef(x) == x * factDef(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 factDef proof function to calculate factDef(3). We would have:
factDef(3) == 3 * factDef(2) //we use fBig, since 3 > 1
factDef(2) == 2 * factDef(1) //we use fBig, since 2 > 1
factDef(1) == 1 //we use fOne Once we work down to:
factDef(1) == 1We can plug 1 in for factDef(1) in factDef(2) == 2 * factDef(1), which gives us:
factDef(2) == 2Similarly, we can plug 2 in for factDef(2) in factDef(3) == 3 * factDef(2), and see that:
factDef(3) == 6Using Logika facts as justifications
If we had our Logika fact, factDef, then we could pull its two definitions into a logic block like this:
l"""{
1. factDef(1) == 1 fact fOne
2. ∀x: Z x > 1 → factDef(x) == x * factDef(x - 1) fact fBig
}"""Note that we must pull in the definitions EXACTLY as they are written in the proof function. The justification is always fact followed by the name of the corresponding 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:
import org.sireum.logika._
// 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, factDef, defines the factorial operation:
l"""{
fact
def factDef(n: Z): Z
fOne. factDef(1) == 1
fBig. ∀x: Z x > 1 → factDef(x) == x * factDef(x - 1)
}"""And we will use factDef to define what we mean by “factorial” in our factorial function contract:
def factorial(n: Z): Z = {
l"""{
requires n >= 1 //factorial(n) is only defined when n >= 1
ensures result == factDef(n) //we promise to return factDef(n),
//where factDef(n) defines n!
}"""
//code for factorial function
}Writing a loop invariant block using a Logika fact
We can similarly use factDef 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 == factDef(i). Since the factDef 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) {
l"""{
invariant product == factDef(i)
i >= 1
modifies i, product
}"""
//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
factorialpostcondition - Prove the precondition holds in the calling code just before calling
factorial - Use the postcondition after calling
factorialto prove the final assert
Here is the completed verification:
import org.sireum.logika._
l"""{
fact
def factDef(n: Z): Z
fOne. factDef(1) == 1
fBig. ∀x: Z x > 1 → factDef(x) == factDef(x - 1) * x
}"""
def factorial(n: Z): Z = {
l"""{
requires n >= 1
ensures result == factDef(n)
}"""
var i: Z = 1 //how many multiplications we have done
var product: Z = 1 //my current calculation
//Prove invariant before loop begins
l"""{
1. i == 1 premise
2. product == 1 premise
//pull in first Logika fact rule
3. factDef(1) == 1 fact fOne
//proves first loop invariant holds
4. product == factDef(i) algebra 1 2 3
//proves second loop invariant holds
5. i >= 1 algebra 1
}"""
while (i != n) {
l"""{
invariant product == factDef(i)
i >= 1
modifies i, product
}"""
i = i + 1
l"""{
//from "i = i + 1"
1. i == i_old + 1 premise
//loop invariant held before changing i
2. product == factDef(i_old) premise
//rewrite invariant with no "_old"
3. product == factDef(i-1) algebra 1 2
//second loop invariant held before changing i
4. i_old >= 1 premise
//needed for the Logika fact
5. i > 1 algebra 1 4
}"""
product = product * i
//Prove invariant still holds at end of iteration
l"""{
//from "product = product * i"
1. product == product_old*i premise
//from previous logic block
2. product_old == factDef(i-1) premise
//pull in Logika fact
3. ∀x: Z x > 1 → factDef(x) == factDef(x - 1) * x fact fBig
//plug in "i" for "x"
4. i > 1 → factDef(i) == factDef(i - 1) * i Ae 3 i
//from previous logic block
5. i > 1 premise
//i > 1, so get right side of →
6. factDef(i) == factDef(i - 1) * i →e 4 5
7. product == factDef(i-1)*i algebra 1 2
//proves first invariant still holds
8. product == factDef(i) algebra 6 7
//proves first invariant still holds
9. i >= 1 algebra 5
}"""
}
//Prove postcondition
l"""{
1. product == factDef(i) premise //loop invariant
2. !(i != n) premise //loop condition false
3. i == n algebra 2
4. product == factDef(n) algebra 1 3
}"""
return product
}
//////// Test code ///////////
var num: Z = 2
//Prove precondition
l"""{
1. num == 2 premise
2. num >= 1 algebra 1 //proves factorial precondition
}"""
var answer: Z = factorial(num)
l"""{
1. answer == factDef(num) premise //factorial postcondition
2. num == 2 premise
3. answer == factDef(2) algebra 1 2
//pull in Logika fact
4. ∀x: Z x > 1 → factDef(x) == factDef(x - 1) * x fact fBig
//plug in "2" for "x"
5. 2 > 1 → factDef(2) == factDef(2 - 1) * 2 Ae 4 2
6. 2 > 1 algebra
//2 > 1, so use →
7. factDef(2) == factDef(2 - 1) * 2 →e 5 6
//pull in Logika fact
8. factDef(1) == 1 fact fOne
9. factDef(2) == factDef(1) * 2 algebra 7
10. factDef(2) == 2 algebra 8 9
//proves claim in assert
11. answer == 2 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 Logika fact:
l"""{
fact
//defines m * n = m + m + ... + m (n times)
def multDef(m: Z, n: Z): Z
//anything multiplied by 0 is just 0
mult0. ∀ x: Z multDef(x, 0) == 0
multPos. ∀ x: Z (∀ y: Z y > 0 → multDef(x, y) == x + multDef(x, y-1))
}"""We could use this Logika fact in the postcondition and loop invariant block for a multiplication function as follows:
import org.sireum.logika._
l"""{
fact
//defines m * n = m + m + ... + m (n times)
def multDef(m: Z, n: Z): Z
//anything multiplied by 0 is just 0
mult0. A x: Z multDef(x, 0) == 0
multPos. A x: Z (A y: Z y > 0 -> multDef(x, y) == multDef(x, y-1) + x)
}"""
//want to find: num1 + num1 + ... + num1 (a total of num2 times)
def mult(num1: Z, num2: Z): Z = {
l"""{
requires num2 >= 0
ensures result == multDef(num1, num2)
}"""
var answer: Z = 0
var cur: Z = 0
while (cur != num2) {
l"""{
invariant
answer == multDef(num1, cur)
cur >= 0
modifies cur, answer
}"""
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:
l"""{
fact
//defines the nth number in the Fibonacci sequence
//1, 1, 2, 3, 5, 8, 13, ...
def fibDef(n: Z): Z
fib1. fibDef(1) == 1
fib2. fibDef(2) == 1
fibN. ∀ x: Z x > 2 → fibDef(x) == fibDef(x-1) + fibDef(x-2)
}"""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:
l"""{
requires (preconditions)
ensures (postconditions)
}"""(The modifies clause is omitted, as we did not use it in this chapter. We will use the modifies clause in chapter 10.) The preconditions list any requirements your function has about the range of its parameters, and the postconditions describe 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:
l"""{
invariant (loop invariants)
modifies (variable list)
}"""The invariant clause lists all loop invariants, 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.