LARA

In the second lab, you'll be using Stainless to verify properties about some more complicated programs.

You are given 1 week for this assignment.

Deadline: Thursday, Mar. 9, 23:59.

Send your solutions by mail to nicolas.voirol@epfl.ch.

We want to verify an implementation of quickSort here. Consider the following code snippet:

import stainless.lang._
import stainless.collection._
 
object QuickSort {
 
  def isSorted(list: List[BigInt]): Boolean = list match {
    case Cons(x, xs @ Cons(y, _)) => x <= y && isSorted(xs)
    case _ => true
  }
 
  def quickSort(list: List[BigInt]): List[BigInt] = (list match {
    case Nil() => Nil[BigInt]()
    case Cons(x, xs) => par(x, Nil(), Nil(), xs)
  }) ensuring { res => isSorted(res) }
 
  def par(x: BigInt, l: List[BigInt], r: List[BigInt], ls: List[BigInt]): List[BigInt] = ls match {
    case Nil() => quickSort(l) ++ Cons(x, quickSort(r))
    case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2)
  }
}

Your task consists of adding contracts to the quickSort and par functions in order for the postcondition of quickSort to verify.

Hint 1: it may be useful to introduce preconditions! However, you aren't allowed to introduce constraints on the inputs to quickSort.

Hint 2: you may need to introduce extra functions!

Hint 3: in some cases when you want to specify a property on the contents of some list, it is useful to use a quantified formula. For example, to say that some property *p* holds on every element of *list*, you can use

forall(x => list.content.contains(x) ==> p(x))

Now, to make sure your verification was actually valid, make sure that Stainless can prove termination of the previous quickSort implementation. Termination is shown by inferring a *measure* such that each successive recursive call is linked to some decrease in the measure. The measure is specified thanks to the *decreases* keyword. For example, you can show that append terminates as follows (note that Stainless automatically shows List.size as terminating by structural induction):

import stainless.lang._
import stainless.collection._
 
object ListTermination {
  def append[A](l1: List[A], l2: List[A]): List[A] = {
    decreases(l1.size)
    l1 match {
      case Cons(x, xs) => Cons(x, append(xs, l2))
      case Nil() => l2
    }
  }
}

You can invoke Stainless termination by using the –termination argument.

Annotate the quickSort and par functions with *decreases* constructs to specify the ordering. Note that you can use lexicographic orderings here by giving tuple arguments to *decreases*. Lexicographic ordering on a pair of non-negative integers (x1,y1) < (x2, y2) is defined by the relation

  x1 < x2 || (x1 == x1 && y1 < y2)

This ordering extends to n-tuples. You may have encountered it if you examine, in a printed dictionary, the ordering of words of the same length, where the word “pie” comes before the word “pig” because, in the alphabetical ordering,

  'p'=='p' && 'i'=='i' && 'e' < 'g'

import stainless.proof._
import stainless.lang._
import stainless.collection._
 
object QuickSort {
 
  def isSorted(list: List[BigInt]): Boolean = {
    list match {
      case Cons(x, xs @ Cons(y, _)) => x <= y && isSorted(xs)
      case _ => true
    }
  }
 
  def appendSorted(l1: List[BigInt], l2: List[BigInt]): List[BigInt] = {
    require(isSorted(l1) && isSorted(l2) && (l1.isEmpty || l2.isEmpty || l1.last <= l2.head))
    l1 match {
      case Nil() => l2
      case Cons(x, xs) => Cons(x, appendSorted(xs, l2))
    }
  } ensuring { res =>
    isSorted(res) &&
    res.content == l1.content ++ l2.content
  }
 
  def quickSort(list: List[BigInt]): List[BigInt] = {
    decreases(list.size, BigInt(0))
    list match {
      case Nil() => Nil[BigInt]()
      case Cons(x, xs) => par(x, Nil(), Nil(), xs)
    }
  } ensuring { res =>
    isSorted(res) &&
    res.content == list.content
  }
 
  def par(x: BigInt, l: List[BigInt], r: List[BigInt], ls: List[BigInt]): List[BigInt] = {
    require(
      forall((a: BigInt) => l.contains(a) ==> a <= x) &&
      forall((a: BigInt) => r.contains(a) ==> x < a)
    )
    decreases(l.size + r.size + ls.size, ls.size + 1)
 
    ls match {
      case Nil() => appendSorted(quickSort(l), Cons(x, quickSort(r)))
      case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2)
    }
  } ensuring { res =>
    isSorted(res) &&
    res.content == l.content ++ r.content ++ ls.content + x
  }
}