## InsertionSort.scala [raw]

```/* Copyright 2009-2016 EPFL, Lausanne */

import stainless.annotation._
import stainless.lang._

object InsertionSort {
sealed abstract class List
case class Nil() extends List

sealed abstract class OptInt
case class Some(value: Int) extends OptInt
case class None() extends OptInt

def size(l : List) : BigInt = (l match {
case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)

def contents(l: List): Set[Int] = l match {
case Nil() => Set.empty
case Cons(x,xs) => contents(xs) ++ Set(x)
}

def isSorted(l: List): Boolean = l match {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
}

/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
def buggySortedIns(e: Int, l: List): List = {
// require(isSorted(l))
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
}
} ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
// Counterexample for postcondition violation in `buggySortedIns`:
//   when e is:
//     0
//   when l is:
//     Cons(-2147483643, Cons(-2147483644, Nil()))
)
}
```

back