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. 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.

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 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
}

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

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))

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) {
    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.

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) {
    ...
    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.

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) {
    ...
    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
)

Example: programs with no “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))

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) {
        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
)