# LARA

## LABS 02: USING THE STAINLESS VERIFICATION SYSTEM (CONT.)

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

### Deliverable

You are given 1 week for this assignment.

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

### Exercise 1

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

### Exercise 2

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'`

### Solutions

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