Conditional Statements
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. 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.
Motivation
Before we formalize the details of verifying a program with a conditional statement, let’s motivate the topic with an example.
Max program
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
}Max assert
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))Analyzing max
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))Rules for analyzing programs with conditionals
In this section, we will summarize how to analyze programs with conditional statements.
Declaring condition and ¬(condition) as premises
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.
Each branch reaches a different conclusion
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.
Each branch reaches the same conclusion
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
}"""Example: programs with no “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))Nested conditionals
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
}"""