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 Logika to verify a subset of programs that use the Scala language. Specifically, we will study verification of programs with the following features:
The Scala programs we verify should be saved with a .sc extension. To show we are using Logika for verification, the first line of the file should be:
// #Sireum #LogikaThere are two modes in Logika – manual and automatic. In chapters 8 and 9, we will use manual mode. In chapter 10, we will use automatic mode. You will designate the verification mode on the second line of the Scala file (just below // #Sireum #Logika). To specify manual mode, you will write:
//@Logika: --manual --background saveAnd to specify automatic mode, you will delete the --manual from above, like this:
//@Logika: --background saveLogika verification should run automatically as you edit these 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 (All in File)”.
This section contains four sample Scala programs that highlight the different language features that we will work with.
This first example gets a number as input from the user, adds one to it, and prints the result:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
var x: Z = Z.prompt("Enter a number: ")
x = x + 1
println("One more is ", x)A few things to note:
import org.sireum._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.Z.prompt(...) function prints a prompt and returns the integer (Z) that was typed. The parameter to this function is the desired prompt. Alternately, the Z.read() function gets and returns an integer from user input without taking a prompt.var x: Z creates a variable called x of type Z – as with the user input functions, the Z means integerHere is a Scala program that gets a number from the user, and uses an if/else statement to print whether the number is positive or negative/zero:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
val num: Z = Z.prompt("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 num cannot be changed after being initializedOur next program uses a while loop to print the numbers from 10 down to 1:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
var cur: Z = 10
while (cur >= 1) {
println("Next number: ", cur)
cur = cur - 1
}Our final sample program demonstrates sequences (similar to 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. If you create this file, you will see an error about the sequence indices possibly being negative – this code cannot be run without some verification work:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
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
These functions 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 these Scala programs, we will add Deduce 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 Deduce proof block updating all relevant facts.
We have already seen that we must include the import statement:
import org.sireum._Anytime we want to do anything with the Logika proof checker. There are three other import statements that you will commonly use:
import org.sireum.justification._ is needed for any Deduce statements and basic justifications (Premise, etc.)import org.sireum.justification.natded.prop._ is needed for any propositional logic justificationsimport org.sireum.justification.natded.pred._ is needed for any predicate logic justificationsHere is the syntax for a Deduce proof block:
Deduce(
1 ( claim ) by 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 Deduce 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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var x: Z = 6
x = x + 1We could insert a proof block between the two lines to express that x currently has the value 6:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var x: Z = 6
Deduce(
1 ( x == 6 ) by 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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var x: Z = 6
//this proof block is correct -- it captures the current value of x
Deduce(
1 ( x == 6 ) by Premise
)
x = x + 1
//NO! This statement no longer captures the current value of x
Deduce(
1 ( x == 6 ) by Premise
)We can use any of our previous deduction rules in a Logika proof block. For example:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
val x: Z = 6
val y: Z = 7
Deduce(
1 ( x == 6 ) by Premise,
2 ( y == 7 ) by Premise,
3 ( (x == 6) ∧ (y == 7) ) by AndI(1, 2)
)An assert statement in Scala 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.
Each time we use an assert, the Logika proof checker will look to see if we have logically justified the expression being asserted. If we have, we will get a purple check mark indicate that the assert statement has been satisified. If we have not, we will get a red error indicating that the assertion has not been proven.
Note that we are using these assert statements differently 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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
val x: Z = 6
val y: Z = 6
val z: Z = 4
Deduce(
1 (x == 6) by Premise,
2 (y == 6) by Premise,
3 (z == 4) by 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. As with our propositional logic proofs, if we want to use a ∧ operator then we type the symbol &. This & is automatically changed to a ∧ when we view our program, just as it was in our deduction proofs. Similarly, we type ! for NOT in asserts (which displays as ¬) and | for OR (which displays as ∨). However, we are not able to use an implies operator in an assert statement as it is not part of the Scala language (and our asserts are part of the program and not just a proof element).
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))As was mentioned above, 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 Scala 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 = Z.read()
assume (a > 0)
Deduce(
1 (a > 0) by 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 proof 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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var a : Z = Z.read()
assume (a != 0)
Deduce(
1 (a != 0) by Premise
)
var b: Z = 20 / a//...is equivalent to:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var a : Z = Z.read()
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.
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 proof block to evaluate what has happened in the program
program statement
// --> add proof block to evaluate what has happened in the program
program statement
// --> add proof 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 proof block to evaluate what changed on that line of code. We will see more details on these proof blocks throughout the rest of this chapter. Recall that the syntax for those proof blocks looks like:
Deduce(
//@formatter:off
1 ( claim ) by Justification,
...
//@formatter:on
)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 (which eliminates the Logika mode notation and the necessary import statements):
var x: Z = 6
var y: Z = x
//this assert will not hold yet
assert (y == 6)Following our process from above, we add proof blocks after each program statement. In these proof blocks, we start by listing the previous program statement as a premise:
var x: Z = 6
Deduce(
1 ( x == 6 ) by Premise,
)
var y: Z = x
Deduce(
1 ( y == x ) by 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 proof block – so we know we want our second proof block to include the claim y == 6.
Here is the program with the second proof block completed – the assert statement will now hold.
var x: Z = 6
Deduce(
1 ( x == 6 ) by Premise,
)
var y: Z = x
Deduce(
1 ( y == x ) by Premise,
2 ( x == 6 ) by Premise, //established in a previous proof block, and x is unchanged since then
3 ( y == 6 ) by Algebra*(1, 2) //we know y is 6 using the claims from lines 1 and 2
)
//this assert will now hold yet
assert (y == 6)We could have also deleted the first proof block in this example. We would still be able to claim x == 6 as a premise in the last proof block, as x had not changed since being given that value.
We have two deduction rules that involve substitution – Subst_< and Subst_>. 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 ∧, ∨, →, F, ∀, ∃ – in those cases, we will be required to use substitution instead.
Here is the syntax for the Subst_< rule. In the example below, line m must be an equivalence (something equals something else). Line n can be anything.
Deduce(
...
m ( LHS_M == RHS_M ) by SomeJustification,
...
n ( LINE_N ) by SomeJustification,
...
p ( claim ) by Subst_<(m, n),
...
)(claim) rewrites LINE_N by substituting all occurrences of RHS_M with LHS_M. The _< part of the justification name indicates the direction of the find/replace. You can think of it as LHS_M <- RHS_M (showing that RHS_M is coming in for each LHS_M). Here is an example:
Deduce(
1 ( x + 1 == y - 4 ) by SomeJustification,
2 ( x*(x + 1) == (x + 1) + y ) by SomeJustification,
3 ( x*(y - 4) == (y - 4) + y ) by Subst_<(1, 2)
)We wrote line 3 by replacing each occurence of x + 1 with y - 4.
Here is the syntax for the Subst_> rule. Just as with Subst_<, line m must be an equivalence (something equals something else). Line n can be anything.
Deduce(
...
m ( LHS_M == RHS_M ) by SomeJustification,
...
n ( LINE_N ) by SomeJustification,
...
p ( claim ) by Subst_>(m, n),
...
)Here, (claim) rewrites LINE_N by substituting all occurrences of LHS_M with RHS_M. We can think of it as indicating LHS_M -> RHS_M (showing that LHS_M is coming in for each RHS_M). Here is an example:
Deduce(
1 ( x + 1 == y ) by SomeJustification,
2 ( x*y == (x + 1) + y ) by SomeJustification,
3 ( x*(x + 1) == (x + 1) + x + 1 ) by Subst_>(1, 2)
)We wrote line 3 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 proof 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 (this example again eliminates the Logika mode notation and the necessary import statements, which we will continue to do in subsequent examples):
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 proof block:
val x: Z = 4
val y: Z = x + 2
val z: Z = 10 - x
Deduce(
1 ( x == 4 ) by Premise, //assignment of unchanged variable
2 ( y == x + 2 ) by Premise, //assignment of unchanged variable
3 ( z == 10 - x ) by Premise, //assignment of unchanged variable
4 ( y == 4 + 2 ) by Subst_<(1, 2),
5 ( z == 10 - 4 ) by Subst_<(1, 3),
6 ( y == 6 ) by Algebra*(4),
7 ( z == 6 ) by Algebra*(5),
8 ( y == z ) by Subst_>(7, 6),
9 ( y == z ∧ y == 6 ) by AndI(8, 6)
)
//now the assert will hold
assert(y == z & y == 6)Note that we did need to do AndI 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 proof 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:
var x: Z = 4
x = x + 1
//this assert will not hold yet
assert(x == 5)Then we might try to add the following proof blocks:
var x: Z = 4
Deduce(
1 ( x == 4 ) by Premise //from previous variable assignment
)
x = x + 1
Deduce(
1 ( x == x + 1 ) by Premise, //NO! Need to distinguish between old x (right side) and new x (left side)
2 ( x == 4 ) by 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 proof 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 Old(varName) function that refers to the OLD value of a variable called varName, just before the latest update. In the example above, we can use Old(x) in the second proof block to refer to x’s value just before it was incremented. We can now change our premises and finish the verification as follows:
var x: Z = 4
Deduce(
1 ( x == 4 ) by Premise //from previous variable assignment
)
x = x + 1
Deduce(
1 ( x == Old(x) + 1 ) by Premise, //Yes! x equals its old value plus 1
2 ( Old(x) == 4 ) by Premise, //Yes! The old value of x was 4
3 ( x == 4 + 1 ) by Subst_<(2, 1),
4 ( x == 5 ) by 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 proof 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 proof block ends. Moreover, we only ever have one Old value available in a proof block – the variable that was most recently changed. This means we will need proof blocks after each variable mutation to process the changes to any related facts.
Suppose we have the following program:
var x: Z = Z.read()
var y: Z = Z.read()
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:
var x: Z = Z.read()
var y: Z = Z.read()
//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 proof blocks after assignment statements, being careful to update all we know (without using the Old value) by the end of each block:
var x: Z = Z.read()
var y: Z = Z.read()
//the original values of both inputs
val xOrig: Z = x
val yOrig: Z = y
Deduce(
1 ( xOrig == x ) by Premise,
2 ( yOrig == y ) by Premise
)
//swap x and y
val temp: Z = x
x = y
Deduce(
1 ( x == y ) by Premise, //from the assignment statement
2 ( temp == Old(x) ) by Premise, //temp equaled the OLD value of x
3 ( xOrig == Old(x) ) by Premise, //xOrig equaled the OLD value of x
4 ( yOrig == y ) by Premise, //yOrig still equals y
5 ( temp == xOrig ) by Algebra*(2, 3),
6 ( x == yOrig ) by Algebra*(1, 4)
)
y = temp
Deduce(
1 ( y == temp ) by Premise, //from the assignment statement
2 ( temp == xOrig ) by Premise, //from the previous proof block (temp and xOrig are unchanged since)
3 ( yOrig == Old(y) ) by Premise, //yOrig equaled the OLD value of y
4 ( x == xOrig ) by Algebra*(1, 2),
5 ( x == yOrig ) by Premise, //from the previous proof block (x and yOrig are unchanged since)
6 ( x == yOrig ∧ y == xOrig ) by AndI(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 proof block, we express as much as we can about all variables/values in the program. In the first proof 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.
We will see in this section that verifying programs with division and modulo requires extra care.
Recall that Z (int) is the only numeric type for Logika verification, 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 proof block, you must have have shown in a previous proof block that denominator is not 0. The easiest way to do this is to prove the claim: denominator != 0. You are even required to do this when dividing by a constant value that is obviously not zero.
For example, if we do:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
Deduce(
1 ( 2 != 0 ) by 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.
We could have instead claimed that 2 > 0 (again using Algebra*()), which would also prove that the denominator was not 0. However, claims such as 2 > 1 would not be accepted as proof that the denominator wasn’t 0 (at least in Logika’s manual mode).
Be careful when making claims that involve division. For example, the following claim will not validate in Logika:
Deduce(
1 ( x == (x/3)*3 ) by Algebra*()
)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 Scala (and 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 proof block, you must have previously established one of the following:
denominator != 0denominator > 0This must be done even if the denominator is a literal value (like 2), and can be demonstrated in the same way as we did with division.
For example:
Deduce(
1 ( 7 != 0 ) by Algebra*()
)
x = a % 7Consider the following program:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var num: Z = Z.prompt("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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
var num: Z = Z.prompt("Enter positive number: ")
assume(num > 0)
val orig: Z = num
num = num * 2
Deduce(
1 ( num == Old(num) * 2 ) by Premise, //we updated num to be its old value times 2
2 ( orig == Old(num) ) by Premise, //orig equaled the old value of num (before our change)
3 ( num == orig * 2 ) by Algebra*(1, 2), //express the new value of num without referring to "Old"
4 ( 2 != 0 ) by Algebra*(), //needed to use modulo in the assert
5 ( num % 2 == 0 ) by Algebra*(1) //we have showed num is now even (needed for next assert)
)
assert(num % 2 == 0)
num = num + 2
Deduce(
1 ( num == Old(num) + 2 ) by Premise, //we updated num to be its old value plus 2
2 ( Old(num) % 2 == 0 ) by Premise, //from line 5 in previous block, but num has since changed
3 ( num % 2 == 0 ) by Algebra*(1, 2), //we have showed num is still even (needed for next assert)
4 ( Old(num) == orig * 2 ) by Premise, //from line 3 in block above, but num has since changed
5 ( num - 2 == orig * 2 ) by Algebra*(1, 4) //express new value of num without using "Old"
)
assert(num % 2 == 0)
//we have already established that 2!= 0, which is needed to divide by 2
num = num/2 - 1
Deduce(
1 ( num == Old(num) / 2 - 1 ) by Premise, //we updated num to be its old value divided by 2 minus 1
2 ( Old(num) - 2 == orig * 2 ) by Premise, //from line 7 in previous block, but num has since changed
3 ( Old(num) == orig * 2 + 2 ) by Algebra*(2),
4 ( num == (orig * 2 + 2) / 2 - 1 ) by Algebra*(1, 3), //express new value of num without using "Old"
5 ( num == orig + 1 - 1 ) by Algebra*(4),
6 ( num == orig ) by 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 proof block after each variable mutation. Work from the top down:
Add a proof 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 the claim denominator != 0. If you can, avoid using division in proof block claims.
To 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. We will only consider programs with an if/else as opposed to an if/else if. 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 program that finds finds the maximum (max) between two user input numbers (x and y):
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
var x: Z = Z.read()
var y: Z = Z.read()
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
Deduce(
1 ( max == x ) by Premise
)and when we analyze the code in the else-branch, we have:
max = y
Deduce(
1 ( max == y ) by Premise
)These two deductions imply that, when the if/else statements finishes, one or the other property holds true:
if (x > y) {
max = x
Deduce(
1 ( max == x ) by Premise
)
} else {
max = y
Deduce(
1 ( max == y ) by Premise
)
}
Deduce(
//max == x in the IF, max == y in the ELSE
1 ( max == x v max == y ) by 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 v 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:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
var x: Z = Z.read()
var y: Z = Z.read()
var max: Z = 0
if (x > y) {
Deduce(
1 ( x > y ) by Premise //the condition is true
)
max = x
Deduce(
1 ( max == x ) by Premise, //from the "max = x" assignment
2 ( max >= x ) by Algebra*(1),
3 ( x > y ) by Premise, //condition is still true (x and y are unchanged)
4 ( max >= y ) by Algebra*(1,3)
)
} else {
Deduce(
1 ( ¬(x > y) ) by Premise, //the condition is NOT true
2 ( x <= y ) by Algebra*(2)
)
max = y
Deduce(
1 ( max == y ) by Premise, //from the "max = y" assignment
2 ( x <= y ) by Premise, //pulled down from previous proof block (x and y are unchanged)
3 ( max >= x ) by Algebra*(1, 2),
4 ( max >= y ) by Algebra*(1)
)
}
//summary of what just happened
Deduce(
//max == x in the IF, max == y in the ELSE
1 ( max == x ∨ max == y ) by Premise,
2 ( max >= x ) by Premise, //true in BOTH branches
3 ( max >= y ) by Premise, //true in BOTH branches
4 ( max >= x ∧ max >= y ) by AndI(2, 3),
5 ( max >= x ∧ max >= y) ∧ (max == x ∨ max == y ) by AndI(4, 1)
)
assert(max >= x ∧ max >= y ∧ (max == x v 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) {
Deduce(
1 ( C ) by Premise
)
} else {
Deduce(
1 ( ¬(C) ) by 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) {
...
Deduce(
1 ( Q1 ) by SomeJustification //conclusion in if-branch
)
} else {
...
Deduce(
1 ( Q2 ) by SomeJustification //conclusion in else-branch
)
}
Deduce(
1 ( Q1 ∨ Q2 ) by 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) {
...
Deduce(
...
1 ( Q ) by SomeJustification //common conclusion reached in IF
)
} else {
...
Deduce(
1 ( Q ) by SomeJustification //common conclusion reached in ELSE
)
}
Deduce(
1 ( Q ) by Premise //Q was true in both the IF and the ELSE
)Some programs have just an if statement with no else. For example, consider this program to find the absolute value of a number:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
var num: Z = Z.read()
var orig: Z = num
if (num < 0) {
num = num * -1
}
//num is now the absolute value of the original input
//(num is nonnegative and either equals `orig` [the original input] or -1*orig)
assert(num >= 0 ∧ (num == -1*orig ∨ num == orig))Even though an “else” is unnecessary in the implementation, we want an else statement in order to ensure our program works in the case that num is NOT less than 0. Our solution is to add an else statement that is solely to hold a proof block for that branch.
We add an else statement and complete our verification as follows:
// #Sireum #Logika
//@Logika: --manual --background save
import org.sireum._
import org.sireum.justification._
import org.sireum.justification.natded.prop._
var num: Z = Z.read()
var orig: Z = num
Deduce(
1 ( orig == num ) by Premise, //from "orig = num" assignment
2 ( num == orig ) by Algebra*(1) //switch order to match assert
)
if (num < 0) {
num = num * -1
Deduce(
1 ( Old(num) < 0 ) by Premise, //if condition (num just changed)
2 ( num == Old(num) * -1 ) by Premise, //from "num = num * -1" assignment
3 ( orig == Old(num) ) by Premise, //orig did equal num (num just changed)
4 ( num >= 0 ) by Algebra*(1, 2), //a negative number times -1 is nonnegative
5 ( num == -1 * orig ) by Algebra*(2, 3) //needed for last part of assert
)
} else {
//no code - just the proof block
Deduce(
1 ( ¬(num < 0) ) by Premise, //negation of condition
2 ( num == orig ) by Premise, //num is unchanged
3 ( num >= 0 ) by Algebra*(1) //needed for assert
)
}
Deduce(
1 ( num >= 0 ) by Premise, //true in both branches
2 ( num == -1*orig ∨ num == orig ) by Premise //LHS in if, RHS in else
3 ( num >= 0 ∧ (num == -1*orig ∨ num == orig) ) by AndI(1, 2) //match assert
)
//num is now the absolute value of the original input
//(num is nonnegative and either equals `orig` [the original input] or -1*orig)
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) {
Deduce(
1 ( C1 ) by Premise, //outer if condition is true
2 ( C2 ) by Premise //inner if condition is true
)
...
Deduce(
1 ( common ) by SomeJustification,
2 ( Q1 ) by SomeJustification
)
}
else {
Deduce(
1 ( C1 ) by Premise, //outer if condition is true
2 ( ¬(C2) ) by Premise //inner if condition is false
)
...
Deduce(
1 ( common ) by SomeJustification,
2 ( Q2 ) by SomeJustification
)
}
Deduce(
1 ( common ) by Premise, //common conclusion in inner if/else
2 ( Q1 ∨ Q2 ) by Premise //Q1 from inner if, Q2 from inner else
)
} else {
if (C3) {
Deduce(
1 ( ¬(C1) ) by Premise, //outer if condition is false
2 ( C3 ) by Premise //inner if condition is true
)
...
Deduce(
1 ( common ) by SomeJustification,
2 ( Q3 ) by SomeJustification
)
}
else {
Deduce(
1 ( ¬(C1) ) by Premise, //outer if condition is false
2 ( ¬(C3) ) by Premise //inner if condition is false
)
...
Deduce(
1 ( common ) by SomeJustification,
2 ( Q4 ) by SomeJustification
)
}
Deduce(
1 ( common ) by Premise, //common conclusion in inner if/else
2 ( Q3 ∨ Q4 ) by Premise //Q1 from inner if, Q2 from inner else
)
}
Deduce(
1 ( common ) by Premise, //"common" was true in both the outer IF and the outer ELSE
2 ( (Q1 ∨ Q2) ∨ (Q3 ∨ Q4) ) by Premise //(Q1 ∨ Q2) from outer if, (Q3 ∨ Q4) from else
)