Logika: Programming Logics
5. Programming Logic for Assignments and Conditionals

5. Programming Logic for Assignments and Conditionals¶

This course will now transition from developing a sound set of logical deduction rules and their use to correctly prove logical claims, to applying those skills to prove the correctness of programs. If time permits, we may cover the Curry-Howard Isomorphism, which demonstrates that there is a direct relationship between computer programs and mathematical proofs.

5.1. Logic and Domain¶

A logic for programming languages would allow us to reason about out program in a systematic way, it might eliminate the need for programming debugging and in many cases may allow for automatic verification that a program is correct.

Earlier in the course, we discussed what we meant by a logic. A logic is a set of truth preserving rules for a domain, which allow new claims (truths) to be derived from the known truths (premises). We further said a logic is sound if new claims in the logic are also true in the domain. The model (the logic abstraction) must match reality. Finally, we limited ourselves to logics that can be executed by a machine.

Here, the domain is that of programming commands and how they impact our knowledge about values stored in memory. This abstraction models every thing about what a program does as set of values in memory and how each command changes what we know about those memory values. It allows us to ignore details such as where the value is (in cache, main memory or virtual memory) and commands which don’t impact the memory values.

We would like our logic to be able to follow the structure of a program and express truths about the values of variables in the program. To that end, our logic will state claims about variables after each command which impacts the knowledge about them.

program command 1
l"""{ previous claims and
       claims based on program command 1}"""
program command 2
l"""{ previous claims and
       claims based on program command 2}"""
program command 3
l"""{ previous claims and
       claims based on program command 3}"""

We will come up with two kinds of logical rules for the programming domain. The first will be claim-manipulating rules. These rules will allow simplification of existing facts through substation and algebra and are used as justifications in Logika proofs.

Claim-transforming rules, on the other hand, capture the meaning of a programming command and allow the deduction of new claims which hold after command execution. They are not used justifications in a Logika proof, but rather provide information on what extra is generated by the programming command.

5.2. Assignment¶

5.2.1. Assignment without Mutation¶

Let us begin by considering programs with assignments without mutation. A program with this feature is called a single-assignment program.

Consider the code

  import org.sireum.logika._

  val x: Z = 6
  val y: Z = 6
  val z: Z = 4

  assert (x == y & y > z)

If we were to paste this into Sireum-Logika right now, it would not pass. The error would be akin to the assertion at line 7 has not been proven. To prove this we note that every assignment statement creates a new fact, but we need to update the Logika-checker with the new fact using special syntax.

In general, every time there is an assignment, there will be a following Logika proof block updating all relevant facts. However this still will not run. Although we have updated the “fact” of each assignment we have not connected them in any meaningful manner. Lets start with adding a new justification for substitution (subst).

The Substitution Deduction Rule (Claim Manipulator)¶

Given 3 integers a, b, c and the fact a == b ∧ b == c, we would like to be able to express a == c as a valid claim. This is the process of substitution. Substitution preserves truth by replacing one proposition with an equivalent one. In Logika it has two forms:

Syntax: subst1 source target    // ( 1 == LHS, 2 == RHS )

Semeantics: Replace every occurrence of the LHS(RHS) of the source in the target
            with the RHS(LHS) of source

Using the substitution rule, the proof now looks like:

import org.sireum.logika._

val x: Z = 6
l"""{
    1. x = 6 premise  // generated by line 3's assigment
    }"""

val y: Z = 6
l"""{
    1. y = 6 premise  // generated by line 7's assigment
    2. x = 6 premise  // from the proof on line 4 - 6
    3. x = y subst2 1 2
    }"""

val z: Z = 4
l"""{
    1. z = 4  premise  // generated by line 7's assigment
    2. x = y  premise  // from the proof on line 9 - 13
    3. y = 6  premise  // from the proof on line 9 - 13
    }"""

assert (x == y & y > z)

Here the use of substitution on line 12 solves the left hand side of the assertion. However to handle the mathematical relationship of 4 < 6 we will need a different tool.

The Algebra Deduction Rule (Claim manipulator)¶

If given integers a, b, c and a < b ∧ b < c we would like to simplify to a < c. Substitution will not work, as it deals strictly with equalities. Fortunately, there is a powerful deduction rule in Logika called algebra. Algebra knows the equality and inequality relationships between integers. The claim 21. 6 > 4 algebra is perfectly correct in the programing logic proof environment. Algebra correctly evaluates integer addition, subtraction, multiplication, division and modulo.

Algebra uses properties like distributive laws, commutative laws etc. For example, here are some laws for the binary operators, + and * where the operands (arguments) are integers:

(a + b) + c = a + (b + c)           law associativity of +
a + b = b + a                       law commutativity of +
a + 0 = a                           law unit+

(a * b) * c = a * (b * c)           law associativity*
a * b = b * a                       law commutativity*
a * 1 = a                           law unit*

a * (b + c) = (a * b) + (a * c)     law distributive * over +

Lets take a look at the complete proof:

import org.sireum.logika._

val x: Z = 6
l"""{
    1. x = 6 premise
    }"""

val y: Z = 6
l"""{
    1. y = 6 premise
    2. x = 6 premise
    3. x = y subst2 1 2
    }"""

val z: Z = 4
l"""{
    1. z = 4          premise
    2. x = y          premise
    3. y = 6          premise
    4. y > z          algebra 1 3
    5. x = y ∧ y > z  ∧i 2 4
    }"""

assert (x == y & y > z)

Here on line 20 we see the most common use of algebra. Logika is told to use other facts it can find in claim 1 (line 17) and claim 3 (line 19) along with algebra to deduce y > z. In general you will feed algebra the lines that allow Logika to calculate the value (or value range) of each var or val in the claim.

All the claims you pass to algebra must be in the current proof. Passing too many, or irrelevant claims generally does no harm. For example, y > z algebra 1 2 3 would still work but the fact that x = y is not helpful. If your claims are insufficient (y > z algebra 1 2), you will receive an error.

Astute readers may have noticed that algebra can often be use in place of substitution. In fact, line 12 can be written as 3. x = y algebra 1 2. Algebra has rules for integer (in)equalities and “common” mathematical operations. It will also handle ¬, as in ¬ (x == 0) which evaluates as `` x != 0``. However, algebra cannot handle any claim involving ∧, ∨, →, ⊥, ∀, ∃. For these you will have to use substitution to build compound/complex claims.

Next, we use ∧i to create a claim which exactly matches the boolean assertion in line 24. Exactly means exactly. If you need assert( x == 6) and you have a claim of 6 = x; it will not work. Likewise, assert ( p | q) will not match q ∨ p.

Here is another quick example.

 val hours: Z = 4
 l"""{ 1.  hours == 4          premise // (generated by the assignment)
 }"""
 val minutes: Z = hours * 60
 l"""{
   1.  hours == 4             premise  // (the last-stated fact, unaltered)
   2.  minutes == hours * 60  premise   // (the fact generated by the assignment)
   3.  minutes == 240         algebra 1 2
 }"""
 assert(minutes = 240)

Logika, Algebra and Division (Modulo)¶

There are three things to note about division (or modulo) when using variables and integer types. First Logika can be finicky about division by a var.

Second, Logika requires you to prove the denominator is not zero before the division. You must prove exactly denominator != 0. Other forms, denominator > 0 or 0 != denominator will not work. This leads to silly looking but necessary statements like

...
14 . 2 != 0   algebra
}"""
var c: Z = a / 2

Finally, Logika KNOWS integer division. 165. (a/5) * 5 = a algebra is not true. You are doing integer math and need to account for the remainder.

import org.sireum.logika._

val a: Z = readInt()
l"""{
     2. 3 != 0 algebra
}"""

assert (a == (a % 3) * 3)

In the above examples, the program correctly fails to verify.

5.2.2. Utility Claim Transformers¶

Often in logic and programming, we need helper functions, previously proved sub-proofs, lemmas etc. to make the work easier. In this course, the Logika commands assume and assert fit in this niche. You have already seen assert in use, so now is an opportune time to more formally introduce the claim-transformation rules for both.

Law for Assume (Claim Transformer)¶

An assume statement, assume (expression), consists of the keyword assume and an expression. If the expression is satisfiable, then the expression is entered as a premise in the following Logika proof-block.

var a: Z = readInt()
assume (a > 0 )
l"""{
     1. a > 0 premise
}"""

You will see a Logika error if the assumption is not satisfiable.

Toy programs often use assume in lieu of wrapping code in an “if statement”

var a : Z = readInt()
assume (a != 0)
l"""{
     1. a != 0  premise
}"""
var b = 20 / a

// instead of
var a : Z = readInt()
var b : Z = 0
if (a != 0) {
   b = 20 / a
}

Law for Assert (Claim Transformer)¶

The assert statement, assert(expression), consists of the keyword assert and an expression. If the expression is true, then the expression is entered as a premise in the following Logika proof-block. If the expression is not true Logika throws an error.

This expression is often used to “prove” that a block of code had the intended effect. It is helpful when “backwards reasoning” (see below) through a program.

...
l"""{
    ... // prove exp
    100. exp    justification
}"""
assert(exp)
l"""{
    1. exp      premise
}"""

With these utility functions in hand, we can get back to our development of claim-transforming rules for assignment.

5.2.3. Assignment with Mutation¶

What we have discussed so far works great for values (named memory locations which are immutable), but does not address the much more common computer programming practice of using mutable locations (or variables). Logika supports variables, and the following program is valid.

import org.sireum.logika._

var x: Z = readInt(" Enter an integer greater than 0 :")
assume (x > 0)
l"""{
      1. x > 0 premise
    }"""
x = 2
l"""{
     1. x = 2 premise
     2. x > 1 algebra 1
     }"""

assert (x > 1)

But this approach quickly breaks down when you consider:

import org.sireum.logika._

var x: Z = readInt(" Enter an integer greater than 0 :")
assume (x > 0)
l"""{
      1. x > 0 premise
    }"""
x = x + 1
l"""{
     1. x = x + 1 premise????
     2. ????
     }"""

assert (x > 1)

While x = x + 1 makes perfect sense in programming languages, it is utter rubbish in logic. Instead we need different rules and more precise way of reasoning about assignment.

Law for Assignment: Forwards Reasoning (Claim Transformer)¶

In the assignment, x = x + 1, we must distinguish between the “old” value of x, which appears on the assignment’s right-hand side, and its “new” value, which appears on its left-hand side. With this distinction, we can reason correctly about x. Here is the example repeated, with the distinction made clear:

import org.sireum.logika._

var x: Z = readInt(" Enter an integer greater than 0 :")
assume (x > 0)
l"""{
      1. x > 0 premise
    }"""
x = x + 1
l"""{
     0. x_old > 0 premise
     1. x = x_old +1 premise
     2. x_old = x -1 algebra 1
     3. x - 1 > 0 algebra 2 0
     4. x > 1 algebra 3
     }"""
assert (x > 1)

When we have an assertion, P(x), that holds true just before an assignment, x = f(x), we calculate the assertions after the assignment, in two stages:

We assert that x = [x_old/x]f(x) and also [x_old/x]P(x). The notation, [x_old/x]E, means that we substitute (replace) all occurrences of x within expression f(x) by x_old.
We next apply deductions, giving us a new assertion, Q(x), that does not mention x_old. This assertion can be carried forwards as a premise for future deduction.

This is what we did in the earlier example – we deduced x > 1, which we can carry forwards. We then forget all the assertions that mentioned x_old.

NOTE: It is vitally important you update all facts which depend on x_old before you exit the Logika proof block following the assignment which caused it to exists. The scope of x_old is only that first Logika proof after the assignment.

The rule’s schematic looks likes this:

l"""{
  ...
  m. P
}"""
x = e
l"""{
  1. x == [x_old/x]e      premise
  2. [x_old/x]P           premise
  ...
  n. Q                    // (where  Q  must _not_ mention  x_old)
}"""

Here is a second example that shows the form of reasoning we follow when working with assignments. Say that y > x at the outset, and we wish to preserve this property as the computation progresses. We can prove it with algebra:

import org.sireum.logika._

 var x: Z = readInt("Enter an int")
   var y: Z = readInt("Enter LARGER int")
   assume (y > x)
   l"""{ 1.  y > x         premise }"""
   x = x - 1
   l"""{
     1.  y > x_old        premise
     2.  x == x_old - 1   premise
     3.  x_old == x + 1   algebra 2    // This line abbreviates multiple small steps.
     4.  y > x + 1        subst1 3 1   // Substitute the equality on line 3 into the formula on line 1.
     5.  y > x            algebra 4    // There is no mention of  x_old
   }"""
   y = y + 1
   l"""{
     1. y_old > x         premise
     2. y == y_old + 1    premise
     3. y > x             algebra 1 2  // This line abbreviates these steps:
                                       //   y_old == y - 1
                                       //   y - 1 > x
                                       //   y > x + 1
   }"""
   assert (y > x)

After each command, a proof segment begins with the premises and then subst and algebra steps lead to the last line, which states the knowledge that travels forwards to the next command. Again, we must ensure that no “_old” variables appear in any claims which we may want to use in subsequent Logika proof blocks as claims.

Here is a third example, where we wish to show that the value within variable x falls in a certain range (perhaps x is used as an index to an array):

import org.sireum.logika._

var x: Z = readInt()
// the precondition is that int  x  falls in the range, 1,2,...,99
assume (x > 0 & x < 100)
l"""{ 1. x > 0 ∧ x < 100           premise    }"""
x = x + 1
l"""{
  1. x_old > 0  ^  x_old < 100     premise
  2. x_old > 0                     ^e1 1
  3. x == x_old + 1                premise
  4. x_old + 1 > 1                 algebra 2
  5. x > 1                         subst2 3 4
  6. x_old < 100                   ^e2 1
  7. x_old + 1 < 101               algebra 6
  8. x < 101                       subst2 3 7
  9. x > 1 ^ x < 101               ^i 5 8
}"""
assert ( x > 1 & x < 101)

The starting assertion about x is sometimes called a precondition, because it is the input property that the program requires to operate successfully. The goal of the program is its postcondition. More on this when we discuss functions and procedures (similar to C# Methods).

Properties Stated in Terms of Initial Input Values¶

Sometimes we really must discuss the “old” value of a variable after an assignment completes. Here is a small but tricky program that swaps the values of the its two variables, x and y:

var x: Z = readInt()
var y: Z = readInt()
val temp: Z = x
x = y
y = temp
println (x, y)

At the end of the program, we want to assert that y has x’s value and x has y’s. To do this, we may invent dummy constants called xin and yin and pretend they are the input values to x and y respectively:

import org.sireum.logika._
 val xin: Z = readInt()
 val yin: Z = readInt()
 var x: Z = xin
 var y: Z = yin
 l"""{
   1. x == xin                                      premise
   2. y == yin                                      premise
 }"""
 val temp: Z = x
 l"""{
   1.  temp == x                                     premise
   3.  x == xin                                     premise
   4.  temp == xin                                  subst1 3 1
 }"""
 x = y
 l"""{
   1. x == y                                         premise
   3. temp == xin                                   premise
   5. y == yin                                      premise
   6. x == yin                                      subst1 5 1
 }"""
 y = temp
 l"""{
   1. y = temp                                       premise
   2. temp = xin                                    premise
   3. y = xin                                       algebra 1 2
   5. x = yin                                       premise
   4. y = xin  ^  x = yin                          ∧i 3 5
   }"""

assert(y == xin  &  x == yin)

The dummy values xin and yin plus the assignment law navigate us through the deduction.

Mechanical Decidability of Properties of Assignment Code¶

After several examples, we are tempted to conclude that deducing forwards knowledge is a mechanical activity, where we do an assignment and then eliminate occurrences of the “old” variable, like this:

l"""{ P }"""
x = e
l"""{
  1.  [x_old/x]P        premise
  2. x == [x_old/x]e    premise

  // solve for  x_old  in terms of  x  and  e :
  3. x_old = ...x...    algebra 2

  // eliminate  x_old  in Line 1 :
  4. [...x.../x_old]P       subst1 3 1
}"""

We can apply this pattern to an earlier example – it works!

import org.sireum.logika._
var x: Z = readInt()
assume (x > 0 & x < 100)
x = x + 1
l"""{
  1. x_old > 0  ^  x_old < 100     premise
  2. x == x_old + 1                premise
  //  Solve for  x_old :
  3. x_old == x - 1                algebra 2
  //  Restate inequalities as atoms
  4. x_old > 0                     ∧e1 1
  5. x_old < 100                   ∧e2 1
  //  Eliminate x_old
  6. x > 1                         algebra 4 3
  7. x < 101                       algebra 5 3
  8. x > 1 ∧ x < 101               ∧i 6 7
}"""
assert (x > 1 & x < 101)

Will the variable-elimination technique always lead us to the final goal? If so, perhaps we can write a proof generator that will automatically write the proofs for us!

Unfortunately, the answer here is “no”. The reason is that important intermediate knowledge can be lost, and here is a simple example that shows how:

var x: Z = readInt()
val y: Z = x * 2
l"""{
       1. y == x * 2        premise
    }"""
x = 3
l"""{
       1. y == x_old * 2       premise
       2. x == 3               premise
       3. x_old == y / 2       algebra 1   // Solve for  x_old
       //  We cannot eliminate  x_old  from  Line 2 ?!
       //  The knowledge that travels forwards is only
       //    x == 3
       //  We lose knowledge about  y.
}"""
val z: Z = 4
// prove here that  y % 2 == 0,  that is,  y is an even-valued int
l"""{
  1. x == 3               premise
  2. z == 4               premise
  // We cannot use   x_old == y / 2  as a premise .... x_old has disappeared.
  // Lines 1 and 2 cannot prove the goal.
}"""

A human sees how to repair the above proof – extract new knowledge about y from premise y == x_old * 2:

import org.sireum.logika._
var x: Z = readInt()
val y: Z = x * 2
l"""{  
     1. y == x * 2        premise 
}"""
x = 3
l"""{
     1. y == x_old * 2       premise
     2. y % 2 == 0           algebra 1   // because  y  is even-valued, even though
                                         // we don't know what value it has
}"""
val z: Z = 4
// prove here that  y % 2 == 0,  that is,  y is an even-valued int
l"""{
     1. y % 2 == 0        premise     //
     2. 2 != 0            algebra     // this line is necessary to avoid an error
                                      // saying we haven't proven divisor is non-zero
}"""
assert (y % 2 == 0)

When we analyze a program in a forwards direction, we work together with an automated checker tool to reach our goal.

5.2.4. Optional Section: The Backwards Law for Assignment and Goal-Directed Reasoning¶

The previous examples raise this question: When we analyze a program from start to finish, which facts should we try to deduce and carry forwards after each assignment? We cannot answer this question unless we know the goal assertion we are trying to prove at the program’s end. For this reason, we should learn how to reason backwards from the goal at the end of a program to the asserts at the beginning. This is called goal-directed reasoning, and there is a simple, beautiful deduction rule for assignments that takes the guesswork out of goal-directed reasoning.

Here is an example. Say that at program’s end, x > 2 must hold, and the program ends like this:

  . . .
l"""{
     subgoal: ???
}"""
x = y + 1
l"""{
    goal: x > 2
}"""

What is the subgoal needed for success? It appears that y > 1 must hold just before the assignment. How did we calculate this? Since the assignment “equates” x with y + 1, it must be y + 1 that is greater than 2 – we substitute y + 1 into the goal, for x, that is, we compute the subgoal as:

[y + 1 / x] (x > 2)  =  (y + 1) > 2

that is, y > 1 is the subgoal:

  . . .
l"""{
     subgoal: y > 1
}"""
x = y + 1
l"""{
    goal: x > 2
}"""

This reasoning is the basis of a “backwards law” for assignment commands.

The formal statement of the backwards-assignment law is this:

l"""{
     subgoal:  [e/x]G
    }"""
x = e
l"""{
    goal: G
    }"""

The goal, G, is sometimes called the assignment’s postcondition, and the subgoal, [e/x]G, is the precondition. It is a formal, proved result that every such precondition, postcondition pair calculated by the backwards-assignment law can be proved as a correct forwards deduction with the forwards-assignment law. Let’s use the backwards assignment law on an example from the previous section.

var x: Z = readInt()
assume (x > 0 & x < 100)
l"""{
     ???
}"""
x = x + 1
l"""{
     x > 1  ^  x < 101   (goal)
}"""
println(x)

The backwards assignment law tells us ???` should be [x + 1/ x](x > 1 ^ x < 101):

var x: Z = readInt()
assume (x > 0 & x < 100)
l"""{
      x + 1 > 1  and  x + 1 < 101  (subgoal)
}"""
x = x + 1
l"""{
     x > 1  ^  x < 101    (goal)
}"""
println(x)

Now, we use algebra to show that the assert proves the subgoal:

var x: Z = readInt()
assume (x > 0 & x < 100)
l"""{
  1. x > 0 ^ x < 100                      premise
  2. x > 0                                ^e1 1
  3. x < 100                              ^e2 1
  4. x + 1 > 1                            algebra 2
  5. x + 1 < 101                          algebra 3
  6. x + 1 > 1  and  x + 1 < 101          ^i 4 5      // (subgoal achieved)
}"""
x = x + 1
l"""{
  1. x_old + 1 > 1  and  x_old + 1 < 101  premise
  2. x == x_old + 1                       premise
  3. x > 1  ^  x < 101                    subst2 2 1 // (goal achived)
}"""
println(x)

The backwards law helps us calculate exactly the correct knowledge at intermediate program points that will lead to the desired final goal.

This technique works well on programs that are sequences of assignments. Here are two examples worked in backwards style:

var dimes: Z = readInt()
var money: Z = dimes * 10
assume WHAT??
dimes = dimes + 1
money = money + 10
// GOAL:   money == dimes * 10

We fill in the subgoals one by one:

var dimes: Z = readInt()
var money: Z = dimes * 10
assume WHAT??
l"""{ SUBGOAL II:  (money + 10) == (dimes + 1) * 10 }"""
dimes = dimes + 1
l"""{ SUBGOAL I:  (money + 10) == dimes * 10 }"""
money = money + 10
// GOAL:   money == dimes * 10

Some algebra simplifies the second subgoal into just money == dimes * 10, which must be asserted at the beginning. Here is a previous problematic example, now neatly handled:

y = x * 2
l"""{
     SUBGOAL II:    y % 2 == 0   (x doesn't matter!)
    }"""
x = 3
l"""{
    SUBGOAL I:     y % 2 == 0   (z doesn't matter!)
}"""
z = 4
// GOAL:   y % 2 == 0,  that is,  y is an even-valued int

The backwards technique works even when there is a self-referential assignment:

var x: Z = readInt()
assume (x > 1)
x = x + 1
l"""{
     goal: x > 2
}"""

We calculate that the subgoal before the assignment must be [x + 1 / x](x > 2), which is (x + 1) > 2. A small algebra step completes the forwards proof of the backwards deduction:

var x: Z = readInt()
assume (x > 1)
l"""{
  1. x > 1            premise
  2. x + 1 > 2        algebra 1
}"""
x = x + 1
l"""{
  1. x = x_old + 1    premise
  2. x_old + 1 > 2    premise
  3. x > 2            subst2 1 2
}"""

By reasoning backwards, we avoid the need to work directly with x_old – the subgoals we calculate by substitution are correctly expressed in terms of x. So, if your program has a clearly stated goal, you can use backwards reasoning to prove that the goal is achieved.

5.3. Conditional Commands¶

To deduce the knowledge generated by a conditional (if-else) command, we must analyze both arms (paths) within the command. This is because some executions will follow the then-arm and some will follow the else-arm. Before we state the rules for forwards and backwards reasoning, we motivate the key ideas with examples. This conditional command sets max to the larger of numbers x and y:

if (x > y) {
    max = x
} else {
    max = y
}

What can we assert when the command finishes, no matter what the values of x and y might be? First, when we analyze the then-arm, we have:

max = x
l"""{
     1. max == x  premise
}"""

and when we analyze the else-arm, we have:

max = y
l"""{
    1. max == y
}"""

These two deductions imply that, when the conditional finishes, one or the other property holds true:

if (x > y) {
    max = x
} else {
    max = y
}
l"""{
     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 arm. 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 conditional was to set max so that it holds the larger of x and y. The assertion we proved so far does not imply the desired goal. This is because we ignored a critical feature of a conditional command: By asking a question — the test — the conditional command generates new knowledge.

For the then arm, we have the new knowledge that x > y; for the else-arm, 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 holds the maximum of x and y:

import org.sireum.logika._

 val x: Z = readInt()
 val y: Z = readInt()
 var max: Z = readInt()
 if (x > y) {
     l"""{
         1. x > y                premise
     }"""
     max = x
     l"""{
       1. x > y                   premise
       2. max == x                premise
       3. max >= x                algebra 2
       4. max >= y                algebra 1 3
       5. max >= x ∧  max >= y   ^i 3 4
     }"""
 } else {
     l"""{
       1. ¬ (x > y)                premise
       2. y >= x                  algebra 1
     }"""
     max = y
     l"""{
       1. max == y                premise
       2. y >= x                  premise
       3. max >= y                algebra 1
       4. max >= x                algebra 1 2
       5. max >= x  ∧  max >= y   ^i 4 3
     }"""
 }
 l"""{
      //1. (max >= x ∧  max >= y) ∨ (max >= x  ∧  max >= y) Logika will not take this
      1. max >= x  ∧  max >= y   premise
 }"""
 assert (max >= x  &  max >= y)

Each arm generates the assertion that max >= x ^ max >= y. Now, in both cases of the or-formula, we can conclude merely max >= x ^ max >= y, as listed in the proof’s last line. This is very similar to OR-elimination from propositional logic.

More accurately stated, the if-else’s proof is <proved in if-branch> v <proved in else-branch>, but Logika’s implementation of the conditional’s claim transformation will not accept the disjunction’s form when the LHS and RHS are exactly the same. Instead this is exactly the as max >= x ^ max >= y.

We are not yet finished with this example; the desired goal is truly:

max >= x  ^  max >= y  ^  (max == x  v  max == y)

You should build a proof of this goal assertion by combining the two partial proofs that we have already constructed.

5.3.1. The Forwards Law for Conditional Commands (Claim Transformation)¶

Here is the schematic of the forwards law for conditionals:

l"""{
    ...
    P
}"""
if (B) {
  l"""{
    1. B          premise
    2. P          premise
    ...
  }"""
  C1
  l"""{
       ...
       Q1
  }"""
} else {
  l"""{
    1. ¬ B         premise
    2. P          premise
    ...
  }"""
  C2
  l"""{
      ...
      Q2
   }"""
}
l"""{
    1. Q1 ∨ Q2   premise
}"""

Note

When both branches of conditional prove the same facts, if(B){ Q1 } else { Q1 }: , Logika will not accept 1. P ∨ P premise if the if-Logika-proof block.

Instead use 1. P premise.

That is, given the assertion, P, at the conditional’s start, the then-arm, C1 uses P and B to generate assertion, Q1, and the else-arm, C2, uses P and ¬B to generate assertion Q2. These two conclusions are joined at the conditional’s conclusion.

When a conditional command lacks an else-arm, e.g.:

if (x < 0 ) {
    x = 0 - x
}

we analyze it without one, using the negation of the if-condition as the only “fact” from the omitted else-branch

import org.sireum.logika._

 var x: Z = readInt()

 if (x < 0) {
 l"""{
       1. x < 0  premise
     }"""

       x = 0 - x
       l"""{
           1. x_old < 0      premise
           2. x = 0 - x_old  premise
           3. x >= 0         algebra 1 2
       }"""
  }
  l"""{
      1. x >= 0 ∨ ¬ (x < 0)  premise
      2.  {
            3. x >= 0        assume
          }
      4.  {
            5. ¬ (x < 0)     assume
            6. x >= 0        algebra 5
          }
      7.   x >= 0            ∨e 1 2 4
  }"""

 assert( x >= 0 )

Here, note on line 18 the negation of the if-condition is used in place of an “else” branch.

5.3.2. Optional Section: The Backwards Law for Conditional Commands¶

Assertions that are disjunctions are cumbersome to handle, and we should avoid them when possible. Given that the forwards law for conditionals generates a disjunction, reflecting the two possibilities for execution, it is important to learn how to reason backwards from a goal through the arms of a conditional command. As usual, we motivate the law through an example. Using the previously seen program that assigns to max, perhaps we want to prove the goal, max >= x ^ max >= y ^ ( max == y V max == x). Our intuition tells us that this goal must be achieved through both paths of the conditional command.

import org.sireum.logika._

val x: Z = readInt()
val y: Z = readInt()
var  max : Z = 0
if (x > y){
     max = x
     } else {
     max = y
     }
assert (max >= x & max >=y & (max == x | max == y))

This can be accomplished this way

First we observe that there are no disjunctions at the top level of the goal so the entire assertion must be proven in both the if- and else-branch. Next we observe that each branch can prove one-side of the max == y V max == x proposition and finally we note which branch uses the if-condition and which the if-condition’s negation.

Another way to look at this same program is might be to say if x > y then max equals x otherwise max equals y. In other words as an implication.

import org.sireum.logika._

val x: Z = readInt()
val y: Z = readInt()
var  max : Z = 0
if (x > y){
     max = x
     } else {
     max = y
     }
assert ((x > y) → (max == x )) ∨ ( ¬ (x > y) → (max == y))

To which we would then “allocate” one side of the top level disjunction to the if-branch and the other to the else-.

import org.sireum.logika._

val x: Z = readInt()
val y: Z = readInt()
var  max : Z = 0
if (x > y){
     max = x
     assert(max == x)
     assert((x >y) → (max == x))
     } else {
     max = y
     assert(max == y)
     assert(¬ (x > y) → (max == y))
     }
assert ((x > y) → (max == x )) ∨ ( ¬ (x > y) → (max == y))

Unfortunately, Logika programs do not understand ¬ , → so it must be written in the disjunctive form of implication

import org.sireum.logika._

val x: Z = readInt()
val y: Z = readInt()
var  max : Z = 0
if (x > y){
     max = x
     assert(max == x)
     assert(!(x > y) | (max == x))
     } else {
     max = y
     assert(max == y)
     assert((x > y) | (max == y))
     }
assert ((!(x > y) | (max == x)) | ((x > y) | (max == y)))

Lets assume you wanted a program to calculate absolute values. Here is an example where incorrect coding will keep you from achieving the desired proof:

 var x: Z = readInt()
 if (x > 0) {
     x = 0 - x
 }
assert( x >= 0)

Using backwards reasoning, we quickly deduce that

var x: Z = readInt()
if(x > 0){
     x = 0 - x
     l"""{
         1. x_old > 0 premise
         2. x = 0 - x_old
         ....
         100. x >= 0   ????
     }
}
l"""{
     1 . x >= 0 ∨ !(x > 0)
     ...
     100. x >= 0  ∨e 1 a b
}"""
assert( x >= 0 )

We see immediately there is no way that the if-subgoal holds true: clearly, (x > 0 → -x > 0) is false, and ¬ (x > 0) → x >= 0 is false also (for values of x that are negative). So, we cannot prove that the program achieves its goal. Forwards reasoning also fails:

var x: Z = readInt()
if (x > 0) {
    l"""{ x > 0 }"""
    x = 0-x
    l"""{
      1. x = 0 - x_old   premise
      2. x_old > 0       premise
      3. x < 0           algebra 1 2
    }"""
}
l"""{
     1. x < 0 ∨ !(x > 0)
     There is no way we can deduce  x >= 0
}"""
assert(x >= 0 )

In contrast, say that we consider this variation of the example:

var x: Z = 0
if(x > 0){
     x = 0 -  x
}
assert(x >=0)

We can prove, using either forwards or backwards reasoning, that this particular program achieves its goal (because we can deduce that the if-branch will be skipped).

5.4. Summary¶

Here are the two laws for reasoning about assignments:

5.4.1. Forwards Assignment Law¶

First, recall that the notation, [a/b]E, denotes phrase E with all occurrences of b replaced by a. (Example: [3 / x](2 * x * x) is (2 * 3 * 3).)

Here is the deduction law for an assignment command:

l"""{
  ...
  m. P
}"""
x = e
l"""{
  1. x == [x_old/x]e      premise
  2. [x_old/x]P           premise
  ...
  n. Q    (where  Q  must _not_ mention  x_old)
}"""

5.4.2. Backwards Assignment Law¶

Given a goal, G, we compute this subgoal:

l"""{ [e/x]G }"""
x = e
l"""{ G }"""

That is, the subgoal (precondition) required to achieve (postcondition) G with the assignment is [e/x]G.

5.4.3. Forwards Conditional Law¶

l"""{ ... P }"""
if (B) {
  l"""{
    1. B          premise
    2. P          premise
    ...
  }"""
  C1
  l"""{ ... Q1  }"""
} else {
  l"""{
    1. ¬B         premise
    2. P          premise
    ...
  }"""
  C2
  l"""{ ... Q2 }"""
}
l"""{ 1. Q1 v Q2   premise }"""
assert ( Q1 | Q2)

That is, if we deduce from precondition B ^ P and commands C1 a postcondition Q1 (and do the same for C2, we can assemble the postcondition Q1 v Q2 for the conditional. (Of course, if Q1 is identical to Q2, we can conclude just Q1.)

5.4.4. Backwards Conditional Law¶

l"""{ (B --> S1)  ^  (¬B --> S2) }"""
if (B) {
  l"""{ S1 }"""
  C1
  l"""{ G }"""
} else {
  l"""{ S2 }"""
  C2
  l"""{ G }"""
}
l"""{ G }"""
assert( G )

That is, if we deduce that S1 is the subgoal required by C1 to attain goal G (similarly for C2), then the subgoal (precondition) needed to attain the goal (postcondition) by the conditional is (B --> S1) ^ (¬B --> S2).

This note was adapted from David Schmidt's CIS 301, 2008, Chapter 2 course note.

It was updated in 2018 by Dr John Hatcliff and George Lavezzi
to conform with Logika syntax and more closely match
KSU's CIS 301 course as taught in Spring 2018.

import	Similar to C# using puts Logika in programming logic mode
val x: Z	Similar to C# const int x val - immutable storage location x - name (start with lower case a - z) Z - integer-type ZS - list of integers (not used here)





assert(bool)	Throws error if boolean statement is false

var x: Z	Similar to C# int x var - mutable storage location x - name (start with lower case a - z) Z - integer-type ZS - list of integers (not used here)





readInt()	Similar to C# Convert.ToInt32(Console.ReadLine());
assume(bool)	Creates a “fact” which can then be used as a premise in the following Logika proof block



assert(bool)	Throws error if boolean statement is false

if (bool){ … }	Similar to C#
if (bool){ … } else { … }	If there is an else branch the if’s ending } must be on the same line as the else {
	There is no else-if. Nest the new if inside the outer-else