Homework 02: Due April 3rd at 10:00 on Moodle

Upload your solution in PDF format to Moodle.

Recall the definition of loop invariants. For the following two problems first find a reasonable precondition and postcondition for the function (in particular, precondition should be as weak as possible to enable correct execution, and postcondition should describe the result as accurately as possible). Then come up with loop invariants that prove that these programs correct.

We are primarily interested in correct precondition, postcondition, and loop invariant. It is in your own interest to prove that the invariants are indeed invariants, otherwise you risk them being wrong. (A formula that is close to an invariant will not be acceptable, it needs to actually satisfy the conditions of an invariant.)

Note on relating initial and final states: If needed, you can introduce auxiliary variables into your program to save the initial version of program state. This will allow you to state precise postcondition that describe how the program state changed in relation to the initial state.

Note on being precise: You can use as much formal notation as you wish, but you need to be precise. By this we mean the following. For preconditions, postconditions, and loop invariants, you must write down a precise formula, using notation such as first-order logic, sets, relation etc. There is no space for writing English, much like we cannot write English instead of Scala and expect Scala Compiler to compile the code into executable bytecodes. In terms of describing proofs, we also suggest that you prove them rigorously: use your intuition to reconstruct the sequence of formal steps that show that verification conditions hold. If you do not do not check by formal derivation that your verification conditions hold, you are doing this at your own risk: it is very likely that you will make a mistake, typically by stating precondition that is too weak. In an informal derivation, your intuition can easily lead you to convince yourself that your program works under those weaker preconditions, when in fact it does not; in such case we will not give you points, because you will be making a mathematically incorrect statement. If you precisely check the verification conditions, you are much more likely to determine whether you have the right preconditions, invariants, and postconditions, and correct them if needed to arrive at a correct solution.

To write down your preconditions, invariants, postconditions, we suggest that you use LaTeX. If you are a beginner with LaTeX, you may it useful to use the LyX document processor built on top of LaTeX, and select the option “View Source” to see how LaTeX works.

Problem 1: List Reversal

The following program computes the reverse of a given list.

case class Node ( var data: Int, var next: Node)
def reverse(l: Node): Node = {
  var temp: Node = null
  var current: Node = l
  var result: Node = null
  while(current != null) {
    temp = current.next
    current.next = result
    result = current
    current = temp
  }
  result
}

To state your invariants, we will instead model the program above using two functions $\text{Next}:\it{Node}\rightarrow \it{Node}$ and $\text{Data}:\it{Node}\rightarrow\it{Int}$ to represent the list. For example consider a list with two elements:

val n0 = Node(5, null)
val n1 = Node(3, n0)

Here the $\text{Next}$ and $\text{Data}$ functions are $\text{Next} = \{(n1,n0),(n0,null)\}$ and $\text{Data} = \{(n0,5),(n1,3)\}$ . Assuming those functions in the program variables the reverse function can be rewritten as the following.

def reverse(l: Node): Node = {
  var temp: Node = null
  var current: Node = l
  var result: Node = null
  while(current != null) {
    temp = Next(current)
    Next = Next(current := result)
    result = current
    current = temp
  }
  result
}

The function essentially reverse the function $\text{Next}$ , except in the last node for which the 'next' field is null.

You should assume the representation using 'Next' function when stating your precondition, postcondition, and loop invariant.

Problem 2: Bubble Sort

The following program sorts a list of integers using the bubble sort algorithm.

def bubblesort( xs : Array[Int]) : Array[Int] = {
  for( i <- 0 until (xs.length - 1))
    for( j <- 0 until (xs.length - i - 1))
      if( xs(j) > xs(j+1)) {
        var tmp = xs(j)
        xs(j) = xs(j + 1)
        xs(j + 1) = tmp
      }
  xs
}

Integer arrays are essentially functions from natural numbers to integers. Using this fact the bubble sort can be rewritten as following:

def bubblesort( Xs : Int => Int, len: Int) : Int => Int = {
  for( i <- 0 until (len - 1))
    for( j <- 0 until (len - i - 1))
      if( Xs(j) > Xs(j+1)) {
        var tmp = Xs(j)
        Xs = Xs(j := Xs(j + 1))
        Xs = Xs(j + 1 := tmp)
      }
  xs
}

You should assume the representation using 'Xs' function when stating your precondition, postcondition, and loop invariants.

Problem 3: The Space of Invariants

Let $S$ be a set (e.g. the set of all integers). Let $Init, Good \subseteq S$ and $r \subseteq S \times S$ . Define

$\begin{equation*} Invs = \{ I \subseteq S \mid Init \subseteq I \land sp(I,r)\subseteq I \land I \subseteq Good \} \end{equation*}$

For each element $I \in Invs$ we have $I \subseteq S$ and we think of $I$ as an invariant.

Prove each of the following statements or give a counterexample. Feel free to answer these parts in any order, but clearly indicate which part is which.

a): If $Invs \neq \emptyset$ , then $sp(Init,r^*) \subseteq Good$ .