For the rest of the course, we will switch gears back to something more familiar for most – computer programs. We will apply the deductive reasoning from the previous chapters in order to prove the correctness of basic programs. This chapter will focus on programs with variable operations, assignments, and conditional statements.
In the next three chapters, we will learn how to reason about different kinds of program structures – assignments, conditional statements, loops, function calls, recursion, lists of elements, and global variables. By the end of chapter 10, we will be able to prove the correctness of simple programs using a toy language that is a subset of Scala. While our toy language is not used in practice, the ideas that we will see to prove program correctness – preconditions, postconditions, loop invariants, and global invariants – can be used to specify functions in ANY language.
We will see that the process for formal specifications and proofs of correctness is rather tedious, even for relatively simple programs. And in practice, proving correctness of computer programs is rarely done. So why bother studying it?
One case where reasoning about correctness is certainly relevant is the arena of safety critical code – where lives depend on a program working correctly. Certain medical devices, such as pacemakers and continuous glucose monitors, have a software component. If that software fails, then a person could die. We can’t test the correctness of medical devices by installing them in a human body and trying them out – instead, we need to be absolutely sure they work correctly before they are used.
Similarly, there is software in things like shuttle launches. While that might not cost lives, it’s also a process that can’t be fully tested beforehand. After all, no one is going to spend over a billion dollar on a “practice” launch. Instead, we need a way to more formally demonstrate that the software will work correctly.
In chapter 9, we will learn to write function specifications. These specifications list any requirements the function has in order to work correctly (preconditions) and descibe the impact of calling the function (postconditions) - most notably, what the function returns in terms of its inputs. Even in cases where we do not formally prove correctness of a program, it is very useful to write a specification for all functions. This can make it clear to any calling code what kinds of parameters should be passed, as well as what to expect about the returned value. By providing this structure, there will be fewer surprises and unintended errors.
As we study program logic, we will use a toy language within Logika. These Logika programs use a subset of the Scala language, and include the following features:
Logika programs should be saved with a .logika extension. To run a Logika program, right-click in the text area that contains the code and select “Run Logika Program”.
There are two modes in Logika – manual and SymExe. In chapters 8 and 9, we will use manual mode. In chapter 10, we will use SymExe mode. You can change the mode in Logika by going to File->Settings->Tools->Sireum->Logika.
For manual mode, uncheck “Auto mode” and mark the Checker kind as “Forward.”
For SymExe mode, check “Auto mode” and mark the Checker kind as “Summarizing SymExe”.
Logika verification should run automatically as you edit Logika programs and their proofs. If a program is verified, you will see a purple checkmark in the lower right corner just as you did in propositional and predicate logic proofs. If there are syntax or logic errors, you will see them highlighted in red.
Sometimes, the Logika verification needs to be run manually. If you don’t see either red errors or a purple checkmark, right-click in the text area that contains the code and select “Logika Check”.
This section contains four sample Logika programs that highlight the different language features.
This first example gets a number as input from the user, adds one to it, and prints the result:
import org.sireum.logika._
var x: Z = readInt("Enter a number: ")
x = x + 1
println("One more is ", x)A few things to note:
import org.sireum.logika._var keyword stands for variable, which is something that can be changed. Logika also has a val keyword, which creates a constant value that cannot be changed.readInt(...) function call is a prompt telling the user what to type. This parameter is optional.var x: Z creates a variable called x of type Z – the Z means integerHere is a Logika program that gets a number from the user, and uses an if/else statement to print whether the number is positive or negative/zero:
import org.sireum.logika._
val num: Z = readInt("Enter a number: ")
if (num > 0) {
println(num, " is positive")
} else {
println(num, " is negative (or zero)")
}A couple of things to note here:
else statement MUST appear on the same line as the closing } of the previous if-statementval keyword in this program means that x cannot be changed after being initializedOur next Logika program uses a while loop to print the numbers from 10 down to 1. This program can’t be run the way it appears below, as Logika wants you to do some verification work first. However, this program demonstrates what a while loop will look like:
import org.sireum.logika._
var cur: Z = 10
while (cur >= 1) {
println("Next number: ", cur)
cur = cur - 1
}Our final sample Logika program demonstrates sequences (Logika’s version of an array or list) and functions. It contains a function, sumSequence, which takes a sequence of integers as a parameter and returns the sum of the numbers in the sequence. At the bottom, we can see our test code that creates a sample sequence and tries calling sumSequence. As in our third example, this code cannot be run without some verification work:
import org.sireum.logika._
def sumSequence(seq: ZS) : Z = {
var sum: Z = 0
var i: Z = 0
while (i < seq.size) {
sum = sum + seq(i)
i = i + 1
}
return sum
}
////// Calling code ////////////
val list: ZS = ZS(1,2,3,4)
val total: Z = sumSequence(list)
println("Sum of elements:", total)A few things of note here:
The definition def sumSequence(seq: ZS) : Z means that a function named sumSequence takes a parameter of type ZS (sequence of integers, Z = int and S = sequence) and returns something of type Z (int)
There is an = after the function header but before the opening { of the function
Functions in Logika are not part of a class - they are more similar to the structure in Python. We can include as many functions as we want in a file. At the bottom of the file (marked below the optional ////// Calling code ////////////) is the calling code. When a Logika program runs, those calling code lines (which may call different functions) are executed. When the calling code lines are done, the program is done.
In order to prove correctness of Logika programs, we will add Logika proof blocks to process what we have learned at different points in the program. In general, every time there is an assignment statement, there will be a following Logika proof block updating all relevant facts.
Here is the syntax for a proof block:
l"""{
lineNumber. claim justification
...
}"""Just as with our propositional and predicate logic proofs, we will number the lines in our proof blocks. Each line will contain a claim and a corresponding justification for that claim. We will still be able to use all of our propositional and predicate logic deduction rules, but we will learn new justifications for processing program statements. Each program may have multiple of these proof blocks to process each assignment statement.
Our first justification in programming logic is premise. In a Logika proof block, we use premise as a justification in the following cases:
To express an assignment statement (or other program statement)
To pull a claim established in a previous proof block into a later proof block
In both cases, the claim must capture the current value of the involved variables.
For example, consider the following program:
import org.sireum.logika._
val x: Z = 6
x = x + 1We could insert a proof block between the two lines to express that x currently has the value 6:
import org.sireum.logika._
val x: Z = 6
l"""{
1. x == 6 premise
}"""
x = x + 1But we could NOT have the same proof block after incrementing x, since x’s value has changed since that claim was established:
import org.sireum.logika._
val x: Z = 6
//this proof block is correct -- it captures the current value of x
l"""{
1. x == 6 premise
}"""
x = x + 1
//NO! This statement no longer captures the current value of x
l"""{
1. x == 6 premise
}"""We can use any of our previous deduction rules in a Logika proof block. For example:
import org.sireum.logika._
val x: Z = 6
val y: Z = 7
l"""{
1. x == 6 premise
2. y == 7 premise
3. (x == 6) ∧ (y == 7) ∧i 1 2
}"""An assert statement in Logika uses the syntax assert(expression), where expression is of type bool. The assert passes if the expression is true, and throws an error if the expression is false.
Logika assert statements are different than assert statements in languages like Java and C# – in those languages, the code in the assert statement (which often includes test method calls) is actually run, and the assert statement checks whether those methods are returning the expected values. In Logika, assert statements only pass if we have previously PROVED what we are claiming – the code is never executed.
Consider the following program:
import org.sireum.logika._
val x: Z = 6
val y: Z = 6
val z: Z = 4
assert (x == y & y > z)While we can tell that x equals y and that y is greater than z, this code would fail in Logika (at least in its manual mode, which is what we are using now). In order for an assert to pass, we must have already proved EXACTLY the statement in the assert.
Why do WE know that x equals y and that y is greater than z? From looking at the code! We can tell that x and y are given the same value (6), and that y’s value of 6 is bigger than z’s value of 4.
So far, we know we can pull in the values of each variable as premises, like this:
import org.sireum.logika._
val x: Z = 6
val y: Z = 6
val z: Z = 4
l"""{
1. x == 6 premise
2. y == 6 premise
3. z == 4 premise
//how to say that x and y are equal, and that y is bigger than z?
}"""
assert (x == y & y > z)But we don’t yet know how to justify claims that describe how variables compare to one another. We will learn how to do that with the algebra and subst rules in section 8.4.
Notice that the program above used an & symbol for an AND operator in an assert statement. Because asserts are part of the program and not part of a proof block, they will use the same conditional operators as in Logika programs. Here is a summary:
| Meaning | Operator in proofs | Operator in Logika programs/assumes/asserts |
|---|---|---|
| p AND q | p ∧ q |
p & q |
| p OR q | p ∨ q |
p | q |
| NOT p | ¬p |
!p |
| p IMPLIES q | p → q |
not available |
If we wanted to write an assert statement that would be true when some variable p was even and/or was a positive two-digit number, we could say:
assert(p % 2 == 0 | (p > 9 & p < 100))The implies operator is not available in assert statements. However, we can make use of one of the equivalences we learned about in section 3.4: that p → q is equivalent to ¬ p ∨ q. So if we wanted to assert that if p was positive, then q was equal to p, then we could write:
//expressing the implicaton ((p > 0) → (q == p))
assert(!(p > 0) | (q == p))Or, equivalently, we could write:
assert((p <= 0) | (q == p))An assume statement in Logika uses the syntax assume(expression). If the expression is satisfiable, then we can use expression as a premise in the following Logika proof block.
For example:
var a: Z = readInt()
assume (a > 0)
l"""{
1. a > 0 premise
}"""Assume statements are almost always used to make assumptions about user input. Perhaps our program only works correctly for certain values of input. If we can assume that the user really did enter acceptable values, then we can use that information (by pulling it in as a premise in the next logic block) to prove the correctness of the program based on that assumption.
Toy programs often use assume in lieu of wrapping code in an if statement. The following two examples are equivalent:
import org.sireum.logika._
var a : Z = readInt()
assume (a != 0)
l"""{
1. a != 0 premise
}"""
var b: Z = 20 / a//...is equivalent to:
import org.sireum.logika._
var a : Z = readInt()
var b : Z = 0
if (a != 0) {
b = 20 / a
}These examples also demonstrate a requirement when we use the division operator in Logika programs, we must first demonstrate that we are not dividing by zero.
You will see an error in Logika if your assume statement is not satisfiable. For example:
import org.sireum.logika._
var a: Z = readInt()
assume(a > 0)
assume (a == 0)If you try verifying this program, you will get a Logika error on the second assume statement. This is because we already assumed that a was greater than 0, and it is not possible for a to also be equal to 0.
In this section, we will learn our first two proof rules for programming logic – algebra and subst.
Before we delve into our new proof rules, let’s look at the process for verifying simple Logika programs (ones that include user input, variable initialization, and assignment statements using different operations). Here, the // --> lines are pieces of the verification process that you must add (or consider) in order to prove correctness of your program, and the other lines are the code of the program.
get user input / set initial variable values
// --> add assume statements to specify what must be true about the input
program statement
// --> add logic block to evaluate what has happened in the program
program statement
// --> add logic block to evaluate what has happened in the program
program statement
// --> add logic block to evaluate what has happened in the program
(...more program statements)
// --> add assert statements to express what our program didWe see that if our program involves user input, then we must consider whether our program will only work correctly for certain input values. In that situation, we express our assumptions using assume statements.
After each program statement, we must add a logic block to evaluate what changed on that line of code. We will see more details on these logic blocks throughout the rest of this chapter. Recall that the syntax for those logic blocks looks like:
l"""{
lineNumber. claim justification
// ... (more claims/justifications)
}"""Finally, we add one or more assert statements to express what our program did. These are usually placed at the end of a program, but sometimes we have assert statements throughout the program to describe the progress up to that point.
The algebra justification can be used for ANY algebraic manipulation on previous claims. When using this justification, include all relevant proof line numbers in whatever order (you might use as few as zero line numbers or as many as 3+ line numbers).
Consider this example:
import org.sireum.logika._
var x: Z = 6
var y: Z = x
//this assert will not hold yet
assert (y == 6)Following our process from above, we add logic blocks after each program statement. In these logic blocks, we start by listing the previous program statement as a premise:
import org.sireum.logika._
var x: Z = 6
l"""{
1. x == 6 premise
}"""
var y: Z = x
l"""{
1. y == x premise
//need claim "y == 6" for our assert to hold
}"""
//this assert will not hold yet
assert (y == 6)For our assert to hold, we must have EXACTLY that claim in a previous logic block – so we know we want our second logic block to include the claim y == 6.
Here is the program with the second logic block completed – the assert statement will now hold.
import org.sireum.logika._
var x: Z = 6
l"""{
1. x == 6 premise
}"""
var y: Z = x
l"""{
1. y == x premise
2. x == 6 premise //established in a previous logic block, and x is unchanged since then
3. y == 6 algebra 1 2 //we know y is 6 using the claims from lines 1 and 2
}"""
//this assert will hold
assert (y == 6)We could have also deleted the first logic block in this example. We would still be able to claim x == 6 as a premise in the last logic block, as x had not changed since being given that value.
We have two deduction rules that involve substitution – subst1 and subst2. Both of these rules are similar to the find/replace feature in text editors. They preserve truth by replacing one proposition with an equivalent one.
The algebra justification will work for most mathematical manipulation. However, it will not work for any claim involving ∧, ∨, →, ⊥, ∀, ∃ – in those cases, we will be required to use substitution instead.
Here is the syntax for the subst1 rule. In the example below, line m must be an equivalence (something equals something else). Line n can be anything.
l"""{
...
m. LHS_M == RHS_M (some justification)
...
n. LINE_N (some justification)
...
p. (claim) subst1 m n
}"""(claim1) rewrites LINE_N by substituting all ocurrences of LHS_M (the FIRST side of line m) with RHS_M. Here is an example:
l"""{
1. x + 1 == y - 4 (some justification)
2. x*(x + 1) == (x + 1) + y (some justification)
3. x*(y - 4) == (y - 4) + y subst1 1 2
}"""We wrote line 2 by replacing each occurence of x + 1 with y - 4.
Here is the syntax for the subst2 rule. Just as with subst1, line m must be an equivalence (something equals something else). Line n can be anything.
l"""{
...
m. LHS_M == RHS_M (some justification)
...
n. LINE_N (some justification)
...
p. (claim) subst2 m n
}"""(claim1) rewrites LINE_N by substituting all ocurrences of RHS_M (the SECOND side of line m) with LHS_M. Here is an example:
l"""{
1. x + 1 == y (some justification)
2. y*(x + 1) == (x + 1) + y (some justification)
3. (x + 1)*(x + 1) == (x + 1) + (x + 1) subst2 1 2
}"""We wrote line 2 by replacing each occurence of y with x + 1. Note that we put parentheses around our first replacement to ensure a product equivalent to the original statement.
Assignment statements in a program come in two forms – with and without mutations. Assignments without mutation are those that give a value to a variable without using the old value of that variable. Assignments with mutation are variable assignments that use the old value of a variable to calculate a value for the variable.
For example, an increment statement like x = x + 1 MUTATES the value of x by updating its value to be one bigger than it was before. In order to make sense of such a statement, we need to know the previous value of x.
In contrast, a statement like y = x + 1 assigns to y one more than the value in x. We do not need to know the previous value of y, as we are not using it in the assignment statement. (We do need to know the value of x).
We have already seen the steps necessary to process assignment statements that do not involve variable mutation. Recall that we can declare as a premise any assignment statement or claim from a previous logic block involving variables that have not since changed.
For example, suppose we want to verify the following program so the assert statement at the end will hold:
import org.sireum.logika._
val x: Z = 4
val y: Z = x + 2
val z: Z = 10 - x
//the assert will not hold yet
assert(y == z & y == 6)Since none of the statements involve variable mutation, we can do the verification in a single logic block:
import org.sireum.logika._
val x: Z = 4
val y: Z = x + 2
val z: Z = 10 - x
l"""{
1. x == 4 premise //assignment of unchanged variable
2. y == x + 2 premise //assignment of unchanged variable
3. z == 10 - x premise //assignment of unchanged variable
4. y == 4 + 2 subst1 1 2
5. z == 10 - 4 subst1 1 3
6. y == 6 algebra 4
7. z == 6 algebra 5
8. y == z subst2 7 6
9. y == z ∧ y == 6 ∧i 8 6
}"""
//now the assert will hold
assert(y == z & y == 6)Note that we did need to do ∧i so that the last claim was y == z ∧ y == 6 , even though we had previously established the claims y == z and y == 6. In order for an assert to hold (at least until we switch Logika modes in chapter 10), we need to have established EXACTLY the claim in the assert in a previous logic block.
Assignments with mutation are trickier – we need to know the old value of a variable in order to reason about its new value. For example, if we have the following program:
import org.sireum.logika._
var x: Z = 4
x = x + 1
//this assert will not hold yet
assert(x == 5)Then we might try to add the following logic blocks:
import org.sireum.logika._
var x: Z = 4
l"""{
1. x == 4 premise //from previous variable assignment
}"""
x = x + 1
l"""{
1. x == x + 1 premise //NO! Need to distinguish between old x (right side) and new x (left side)
2. x == 4 premise //NO! x has changed since this claim
}"""
//this assert will not hold yet
assert(x == 5)…but then we get stuck in the second logic block. There, x is supposed to refer to the CURRENT value of x (after being incremented), but both our attempted claims are untrue. The current value of x is not one more than itself (this makes no sense!), and we can tell from reading the code that x is now 5, not 4.
To help reason about changing variables, Logika has a special name_old value that refers to the OLD value of a variable called name, just before the latest update. In the example above, we can use x_old in the second logic block to refer to x’s value just before it was incremented. We can now change our premises and finish the verification as follows:
import org.sireum.logika._
var x: Z = 4
l"""{
1. x == 4 premise //from previous variable assignment
}"""
x = x + 1
l"""{
1. x == x_old + 1 premise //Yes! x equals its old value plus 1
2. x_old == 4 premise //Yes! The old value of x was 4
3. x == 4 + 1 subst1 2 1
4. x == 5 algebra 3 //Could have skipped line 3 and used "algebra 1 2" instead
}"""
//now the assert will hold
assert(x == 5)By the end of the logic block following a variable mutation, we need to express everything we know about the variable’s current value WITHOUT using the _old terminology, as its scope will end when the logic block ends. Moreover, we only ever have one _old value available in a logic block – the variable that was most recently changed. This means we will need logic blocks after each variable mutation to process the changes to any related facts.
Suppose we have the following Logika program:
import org.sireum.logika._
var x: Z = readInt()
var y: Z = readInt()
val temp: Z = x
x = y
y = temp
//what do we want to assert we did?We can see that this program gets two user input values, x and y, and then swaps their values. So if x was originally 4 and y was originally 6, then at the end of the program x would be 6 and y would be 4.
We would like to be able to assert what we did – that x now has the original value from y, and that y now has the original value from x. To do this, we might invent dummy constants called xOrig and yOrig that represent the original values of those variables. Then we can add our assert:
import org.sireum.logika._
var x: Z = readInt()
var y: Z = readInt()
//the original values of both inputs
val xOrig: Z = x
val yOrig: Z = y
val temp: Z = x
x = y
y = temp
//x and y have swapped
//x has y's original value, and y has x's original value
assert(x == yOrig & y == xOrig) //this assert will not yet holdWe can complete the verification by adding logic blocks after assignment statements, being careful to update all we know (without using the _old value) by the end of each block:
import org.sireum.logika._
var x: Z = readInt()
var y: Z = readInt()
//the original values of both inputs
val xOrig: Z = x
val yOrig: Z = y
l"""{
1. xOrig == x premise
2. yOrig == y premise
}"""
//swap x and y
val temp: Z = x
x = y
l"""{
1. x == y premise //from the assignment statement
2. temp == x_old premise //temp equaled the OLD value of x
3. xOrig == x_old premise //xOrig equaled the OLD value of x
4. yOrig == y premise //yOrig still equals y
5. temp == xOrig algebra 2 3
6. x == yOrig algebra 1 4
}"""
y = temp
l"""{
1. y == temp premise //from the assignment statement
2. temp == xOrig premise //from the previous logic block (temp and xOrig are unchanged since then)
3. yOrig == y_old premise //yOrig equaled the OLD value of y
4. y == xOrig algebra 1 2
5. x == yOrig premise //from the previous logic block (x and yOrig are unchanged since then)
6. x == yOrig ^ y == xOrig ^i 5 4
}"""
//x and y have swapped
//x has y's original value, and y has x's original value
assert(x == yOrig & y == xOrig) //this assert will hold nowNotice that in each logic block, we express as much as we can about all variables/values in the program. In the first logic block, even though xOrig and yOrig were not used in the previous assignment statement, we still expressed how the current values our other variables compared to xOrig and yOrig. It helps to think about what you are trying to claim in the final assert – since our assert involved xOrig and yOrig, we needed to relate the current values of our variables to those values as we progressed through the program.
Working with division and modulo requires extra care, as Logika is finicky about both.
Recall that Z (int) is the only numeric type in Logika, so any division is integer division. This means something like 9/2 evaluates to 4, just as it would in Java or C#.
Before doing division of the form numerator/denominator, either in a line of code or in a logic block, you must have a line in a previous logic block that states: denominator != 0. Other forms, such as denominator > 0 or 0 != denominator, will not work. You are even required to do this when dividing by a constant value that is obviously not zero.
For example, if we do:
import org.sireum.logika._
var x: Z = 10 / 2Then Logika will give us an error complaining we have not proved that the denominator is not zero. We must add the claim 2 != 0 as follows:
import org.sireum.logika._
l"""{
1. 2 != 0 algebra
}"""
var x: Z = 10 / 2Note that our justification is just, algebra, as we don’t need any extra information to claim that 2 is not equal to 0.
Be careful when making claims that involve division. For example, the following claim will not validate in Logika:
l"""{
1. x == (x/3)*3 algebra //NO!
}"""While the claim x == (x/3)*3 is certainly true in math, it is not true with integer division. For example, if x is 7, then (x/3)*3 is 6 – so the two sides are not equal. In general, I recommend avoiding claims involving division if you can at all help it. Instead, try to find a way to express the same idea in a different way using multiplication.
Modulo (%) works the same way in Logika as it does in other programming languages. For example, 20 % 6 evaluates to 2.
Before using the modulo operator in the form numerator % denominator, either in a line of code or as a claim in a logic block, you must have EXACTLY these claims in the previous logic block:
numerator >= 0denominator > 0For example:
...
l"""{
1. 2 > 0 algebra
2. a >= 0 (some justification)
}"""
x = a % 2
...Consider the following Logika program:
import org.sireum.logika._
var num: Z = readInt("Enter positive number: ")
assume(num > 0)
val orig: Z = num
num = num * 2
assert(num % 2 == 0)
num = num + 2
assert(num % 2 == 0)
num = num/2 - 1
assert(num == orig)It can often be handy to walk through a program with sample numbers before trying to prove its correctness:
num, is 11orig is initialized to be 11 alsonum is multiplied by 2, and is 22num would be even, since any number times two is always even (and indeed, 22 is even)num, so it is now 24num would still be even, as it was even before and we added 2 (another even number) to it. Indeed, 24 is still even.num by dividing it by 2 and subtracting 1, so num is now back to its original value of 11 (the same as orig). This step “undoes” the changes we have made to num – looking at the code, we can see that the final value of num is orig*2 + 2, so if we do (orig*2 + 2) / 2 - 1, we are left with orig.Here is the completed verification, with comments at each step:
import org.sireum.logika._
var num: Z = readInt("Enter positive number: ")
assume(num > 0)
val orig: Z = num
num = num * 2
l"""{
1. num == num_old * 2 premise //we updated num to be its old value times 2
2. orig == num_old premise //orig equaled the old value of num (before our change)
3. num == orig * 2 algebra 1 2 //express the new value of num without referring to "_old"
4. 2 > 0 algebra //needed to use modulo in step 7
5. num_old > 0 premise //we assumed the old value of num (before its change) was > 0
6. num >= 0 algebra 1 5 //needed to use modulo in step 7
7. num % 2 == 0 algebra 1 //we have showed num is now even (needed for next assert)
}"""
assert(num % 2 == 0)
num = num + 2
l"""{
1. num == num_old + 2 premise //we updated num to be its old value plus 2
2. num_old >= 0 premise //from line 6 in previous block, but num has since changed
3. num_old % 2 == 0 premise //from line 7 in previous block, but num has since changed
//we know 2 > 0 from previous block - don't need to restate here
4. num >= 0 algebra 1 2 //needed to use modulo in step 5 (need to redo since num has changed)
5. num % 2 == 0 algebra 1 3 //we have showed num is still even (needed for next assert)
6. num_old == orig * 2 premise //from line 3 in block above, but num has since changed
7. num - 2 == orig * 2 algebra 1 6 //express new value of num without using "_old"
}"""
assert(num % 2 == 0)
l"""{
1. 2 != 0 algebra //needed for dividing by 2
}"""
num = num/2 - 1
l"""{
1. num == num_old/2 - 1 premise //we updated num to be its old value divided by 2 minus 1
2. num_old - 2 == orig * 2 premise //from line 7 in previous block, but num has since changed
3. num_old == orig * 2 + 2 algebra 2
4. num == (orig * 2 + 2)/2 - 1 algebra 1 3 //express new value of num without using "_old"
5. num == orig + 1 - 1 algebra 4
6. num == orig algebra 5 //we have showed num is back to being orig (needed for last assert)
//could have skipped straight here with "algebra 1 2"
assert(num == orig)Sometimes it can be tricky to figure out what to do at each step in order to get assert statements to pass. If you are unsure what to do, I recommend:
Walk through the program several times with sample numbers, keeping track of changes to variables. Why do the assert statements make sense to you? Convince yourself that they are valid claims before you worry about the formal verification.
Add a logic block after each variable mutation. Work from the top down:
Add a logic block before each use of division (numerator / denominator) and modulus (numerator % denominator). Pull in claims from previous blocks as described above to help you show what is needed about numerator and denominator:
denominator != 0numerator >= 0 and denominator > 0To deduce the knowledge generated by a conditional (if/else) statement, we must analyze both branches. This is because some executions will follow the if-branch and some will follow the else-branch. Recall that Logika does not have an if/else if statement. However, you can simulate more than two branches by nesting another if/else inside the outer else.
Before we formalize the details of verifying a program with a conditional statement, let’s motivate the topic with an example.
Suppose we have a Logika program that finds finds the maximum (max) between two user input numbers (x and y):
import org.sireum.logika._
val x: Z = readInt()
val y: Z = readInt()
var max: Z = 0 //give max a dummy starting value
if (x > y) {
max = x
} else {
max = y
}Before worrying about how to do the verification, let’s consider what we should assert at the end in order to be sure that max really does hold the biggest of the two inputs. Clearly, max should be greater than or equal to both inputs. So should our assert be:
//Not quite all we want to say
assert(max >= x & max >= y)Suppose x was 10, y was 15…and that max was 20. (Clearly this isn’t what our code would do, but you can imagine writing something else for the max code that came up with such a calculation). In this case, max is indeed greater than or equal to both inputs…but it is just as clearly not the max. We know see that we also need to claim that max equals one of the two inputs. This makes our assert:
//Now we are sure we are describing the max between x and y
assert(max >= x & max >= y & (max == x | max == y))Now, we need to prove that our assert holds no matter which branch we follow in the conditional statement. First, when we analyze the code in the if-branch, we have:
max = x
l"""{
1. max == x premise
}"""and when we analyze the code in the else-branch, we have:
max = y
l"""{
1. max == y premise
}"""These two deductions imply that, when the if/else statements finishes, one or the other property holds true:
if (x > y) {
max = x
l"""{
1. max == x premise
}"""
} else {
max = y
l"""{
1. max == y premise
}"""
}
l"""{
//max == x in the IF, max == y in the ELSE
1 . max == x v max == y premise
}"""This illustrates the first principle of conditional commands: the knowledge produced by the command is the disjunction (or) of the knowledge produced by each branch. In the section on propositional logic, we covered how to apply cases analyses on disjunctive assertions to extract useful knowledge.
Recall that the intent of the if/else statement was to set max so that it holds the larger of x and y, so that our assert would hold:
assert(max >= x & max >= y & (max == x | max == y))The claim we proved so far satisifies the second part of our assert statement, but not the first part. This is because we ignored a critical feature of an if/else statement: By asking a question — the condition — the if/else statement generates new knowledge.
For the if-branch, we have the new knowledge that x > y; for the else-branch, we have that ¬(x > y), that is, y >= x. We can embed these assertions into the analysis of the conditional command, like this, and conclude that, in both cases, max is greater than or equal to both inputs:
import org.sireum.logika._
var x: Z = readInt()
var y: Z = readInt()
var max: Z = 0
if (x > y) {
l"""{
2. x > y premise //the condition is true
}"""
max = x
l"""{
1. max == x premise //from the "max = x" assignment
2. max >= x algebra 1
3. x > y premise //condition is still true (x and y are unchanged)
4. max >= y algebra 1 3
}"""
} else {
l"""{
2. ¬(x > y) premise //the condition is NOT true
3. x <= y algebra 2
}"""
max = y
l"""{
1. max == y premise //from the "max = y" assignment
2. x <= y premise //pulled down from previous logic block (x and y are unchanged)
3. max >= x algebra 1 2
4. max >= y algebra 1
}"""
}
//summary of what just happened
l"""{
//max == x in the IF, max == y in the ELSE
1. max == x ∨ max == y premise
2. max >= x premise //true in BOTH branches
3. max >= y premise //true in BOTH branches
4. max >= x ∧ max >= y ^i 2 3
5. (max >= x ∧ max >= y) ∧ (max == x ∨ max == y) ^i 4 1
}"""
assert((max >= x & max >= y) & (max == x | max == y))In this section, we will summarize how to analyze programs with conditional statements.
If we have a program such as this with an if/else statement:
if (C) {
} else {
}Then we can claim C as a premise immediately inside the if-branch and ¬(C) as a premise immediately inside the else branch:
if (C) {
l"""{
1. C premise
}"""
} else {
l"""{
1. ¬(C) premise
}"""
}Be careful with the else case – you must claim exactly ¬(C), and not some claim you know to be equivalent. In our max example, C was x < y, and we needed to claim exactly ¬(x < y) in the else – NOT x >= y. After you have pulled in the initial claim using the form ¬(C), you can use algebra to manipulate it into a different form.
If the if-branch reaches conclusion Q1 and the else branch reaches conclusion Q2, then afterwards we can list as a premise that one of those conclusions is true (since we know that one of the branches in an if/else will ALWAYS execute):
if (C) {
...
l"""{
...
1. Q1 (some justification) //conclusion in if-branch
}"""
} else {
l"""{
...
1. Q2 (some justification) //conclusion in else-branch
}"""
}
l"""{
1. Q1 ∨ Q2 premise //Q1 from if, Q2 from else
}"""Note that order matters, and that we must claim (if conclusion) ∨ (else conclusion) – in the example above, we could not claim Q2 ∨ Q1 afterwards.
If the if-branch and the else-branch both reach the SAME conclusion Q, then afterwards we can list Q as a premise. Here, we know that one of the branches in an if/else will ALWAYS execute – so if we get to the same conclusion in both cases, then we must always reach that conclusion:
if (C) {
...
l"""{
...
1. Q (some justification) //common conclusion reached in IF
}"""
} else {
l"""{
...
1. Q (some justification) //common conclusion reached in ELSE
}"""
}
l"""{
1. Q premise //Q was true in both the IF and the ELSE
}"""Suppose we have an if-statement with no “else”. Afterwards, we know that either the if-branch was executed (which happens when the condition is true), or that the condition was false. If we reach some conclusion Q in the if-branch, then afterwards we know that either Q is true or that the if-statemention condition is not true. Similarly, if some claim old was true before an if-statement without an else, then afterwards we know that we either reached Q in the if-branch or that our old statement is still true.
We can pull in these claims as premises after an if-statement as follows:
l"""{
1. old (some justification)
}"""
if (C) {
...
l"""{
...
1. Q (some justification) //conclusion in if-branch
}"""
}
l"""{
1. Q ∨ ¬(C) premise //either we reached Q in the if, or the condition was false
2. Q ∨ old premise //either we reached Q in the if, or "old" is still true
}"""For example, suppose we have a program that finds the absolute value of an input number:
import org.sireum.logika._
var num: Z = readInt()
var orig: Z = num
if (num < 0) {
num = num * -1
}
//num is now the absolute value of the original inputAfterwards, we want to assert that num is the absolute value of the original input – that num is nonnegative and either equals orig (the original input) or -1*orig:
assert(num >= 0 & (num == -1*orig | num == orig))We start our verification as follows:
import org.sireum.logika._
var num: Z = readInt()
val orig: Z = num
l"""{
1. orig == num premise //from "orig = num" assignment
2. num == orig algebra 1 //switch order to match assert
}"""
if (num < 0) {
num = num * -1
l"""{
1. num_old < 0 premise //if condition (num just changed)
2. num == num_old * -1 premise //from "num = num * -1" assignment
3. orig == num_old premise //orig did equal num (num just changed)
4. num >= 0 algebra 1 2 //a negative number times -1 is nonnegative
5. num == -1*orig algebra 2 3 //needed for last part of assert
}"""
}
l"""{
1. num >= 0 ∨ ¬(num < 0) premise //conclusion from if OR !(condition)
2. num == -1*orig ∨ num == orig premise //conclusion from if OR num still equals orig
//incomplete
}"""
//num is now nonnegative
assert(num >= 0 & (num == orig | num == -1*orig))In our final logic block, we need to reach the claim num >= 0 so we can combine it with num == -1*orig ∨ num == orig to match our assert. We can do this with OR elimination on num >= 0 ∨ ¬(num < 0):
import org.sireum.logika._
var num: Z = readInt()
val orig: Z = num
l"""{
1. orig == num premise //from "orig = num" assignment
2. num == orig algebra 1 //switch order to match assert
}"""
if (num < 0) {
num = num * -1
l"""{
1. num_old < 0 premise //if condition (num just changed)
2. num == num_old * -1 premise //from "num = num * -1" assignment
3. orig == num_old premise //orig did equal num (num just changed)
4. num >= 0 algebra 1 2 //a negative number times -1 is nonnegative
5. num == -1*orig algebra 2 3 //needed for last part of assert
}"""
}
l"""{
1. num >= 0 ∨ ¬(num < 0) premise //conclusion from if OR !(condition)
2. num == -1*orig ∨ num == orig premise //conclusion from if OR num still equals orig
3. {
4. num >= 0 assume
}
5. {
6. ¬(num < 0) assume
7. num >= 0 algebra 6
}
8. num >= 0 ∨e 1 3 5
9. num >= 0 ∧ (num == -1*orig ∨ num == orig) ∧i 8 2 //match assert
}"""
//num is now nonnegative
assert(num >= 0 & (num == -1*orig | num == orig))We employ the same rules when analyzing programs with nested conditional statements. If we reach a common conclusion in both the if and else branches of an inner if/else statement, for example, then we can claim the common conclusion as a premise after that inner if/else statement (but still inside the outer if/else). The outline below summarizes what we can claim at various places in nested if/else statement:
if (C1) {
if (C2) {
l"""{
1. C1 premise //outer if condition is true
2. C2 premise //inner if condition is true
}"""
...
l"""{
1. common (some justification)
2. Q1 (some justification)
}"""
}
else {
l"""{
1. C1 premise //outer if condition is true
2. ¬(C2) premise //inner if condition is false
}"""
...
l"""{
1. common (some justification)
2. Q2 (some justification)
}"""
}
l"""{
1. common premise //common conclusion in inner if/else
2. Q1 ∨ Q2 premise //Q1 from inner if, Q2 from inner else
}"""
} else {
if (C3) {
l"""{
1. ¬(C1) premise //outer if condition is false
2. C3 premise //inner if condition is true
}"""
...
l"""{
1. common (some justification)
2. Q3 (some justification)
}"""
}
else {
l"""{
1. ¬(C1) premise //outer if condition is false
2. ¬(C3) premise //inner if condition is false
}"""
...
l"""{
1. common (some justification)
2. Q4 (some justification)
}"""
}
l"""{
1. common premise //common conclusion in inner if/else
2. Q3 ∨ Q4 premise //Q1 from inner if, Q2 from inner else
}"""
}
l"""{
1. common premise //"common" was true in both the outer IF and the outer ELSE
2. (Q1 ∨ Q2) ∨ (Q3 ∨ Q4) premise //(Q1 ∨ Q2) from outer if, (Q3 ∨ Q4) from else
}"""