testcase folder for regist master thesis results

testcases/master-thesis-regis/Arithmetic.scala

+import leon.Utils._
+
+object Arithmetic {
+
+  /* VSTTE 2008 - Dafny paper */
+  def mult(x : Int, y : Int): Int = ({
+    var r = 0
+    if(y < 0) {
+      var n = y
+      (while(n != 0) {
+        r = r - x
+        n = n + 1
+      }) invariant(r == x * (y - n) && 0 <= -n)
+    } else {
+      var n = y
+      (while(n != 0) {
+        r = r + x
+        n = n - 1
+      }) invariant(r == x * (y - n) && 0 <= n)
+    }
+    r
+  }) ensuring(_ == x*y)
+
+  /* VSTTE 2008 - Dafny paper */
+  def add(x : Int, y : Int): Int = ({
+    var r = x
+    if(y < 0) {
+      var n = y
+      (while(n != 0) {
+        r = r - 1
+        n = n + 1
+      }) invariant(r == x + y - n && 0 <= -n)
+    } else {
+      var n = y
+      (while(n != 0) {
+        r = r + 1
+        n = n - 1
+      }) invariant(r == x + y - n && 0 <= n)
+    }
+    r
+  }) ensuring(_ == x+y)
+
+  /* VSTTE 2008 - Dafny paper */
+  def addBuggy(x : Int, y : Int): Int = ({
+    var r = x
+    if(y < 0) {
+      var n = y
+      (while(n != 0) {
+        r = r + 1
+        n = n + 1
+      }) invariant(r == x + y - n && 0 <= -n)
+    } else {
+      var n = y
+      (while(n != 0) {
+        r = r + 1
+        n = n - 1
+      }) invariant(r == x + y - n && 0 <= n)
+    }
+    r
+  }) ensuring(_ == x+y)
+
+  def sum(n: Int): Int = {
+    require(n >= 0)
+    var r = 0
+    var i = 0
+    (while(i < n) {
+      i = i + 1
+      r = r + i
+    }) invariant(r >= i && i >= 0 && r >= 0)
+    r
+  } ensuring(_ >= n)
+
+}

testcases/master-thesis-regis/ArrayOperations.scala

+import leon.Utils._
+
+object ArrayOperations {
+
+  /* VSTTE 2008 - Dafny paper */
+  def binarySearch(a: Array[Int], key: Int): Int = ({
+    require(a.length > 0 && sorted(a, 0, a.length - 1))
+    var low = 0
+    var high = a.length - 1
+    var res = -1
+
+    (while(low <= high && res == -1) {
+      val i = (high + low) / 2
+      val v = a(i)
+
+      if(v == key)
+        res = i
+
+      if(v > key)
+        high = i - 1
+      else if(v < key)
+        low = i + 1
+    }) invariant(
+        res >= -1 &&
+        res < a.length &&
+        0 <= low && 
+        low <= high + 1 && 
+        high >= -1 &&
+        high < a.length && 
+        (if (res >= 0) 
+            a(res) == key else 
+            (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
+        )
+       )
+    res
+  }) ensuring(res => 
+      res >= -1 && 
+      res < a.length && 
+      (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))
+
+
+  def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+    require(a.length >= 0 && to <= a.length && from >= 0)
+    def rec(i: Int): Boolean = {
+      require(i >= 0)
+      if(i >= to) 
+        false 
+      else {
+       if(a(i) == key) true else rec(i+1)
+      }
+    }
+    if(from >= to)
+      false
+    else
+      rec(from)
+  }
+
+  def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+    require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+    var k = l
+    var isSorted = true
+    (while(k < u) {
+      if(a(k) > a(k+1))
+        isSorted = false
+      k = k + 1
+    }) invariant(k <= u && k >= l)
+    isSorted
+  }
+
+  /* The calculus of Computation textbook */
+  def bubbleSort(a: Array[Int]): Array[Int] = ({
+    require(a.length >= 1)
+    var i = a.length - 1
+    var j = 0
+    val sa = a.clone
+    (while(i > 0) {
+      j = 0
+      (while(j < i) {
+        if(sa(j) > sa(j+1)) {
+          val tmp = sa(j)
+          sa(j) = sa(j+1)
+          sa(j+1) = tmp
+        }
+        j = j + 1
+      }) invariant(
+            j >= 0 &&
+            j <= i &&
+            i < sa.length &&
+            sa.length >= 0 &&
+            partitioned(sa, 0, i, i+1, sa.length-1) &&
+            sorted(sa, i, sa.length-1) &&
+            partitioned(sa, 0, j-1, j, j)
+          )
+      i = i - 1
+    }) invariant(
+          i >= 0 &&
+          i < sa.length &&
+          sa.length >= 0 &&
+          partitioned(sa, 0, i, i+1, sa.length-1) &&
+          sorted(sa, i, sa.length-1)
+       )
+    sa
+  }) ensuring(res => sorted(res, 0, a.length-1))
+
+  def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+    require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
+    if(l2 > u2 || l1 > u1)
+      true
+    else {
+      var i = l1
+      var j = l2
+      var isPartitionned = true
+      (while(i <= u1) {
+        j = l2
+        (while(j <= u2) {
+          if(a(i) > a(j))
+            isPartitionned = false
+          j = j + 1
+        }) invariant(j >= l2 && i <= u1)
+        i = i + 1
+      }) invariant(i >= l1)
+      isPartitionned
+    }
+  }
+
+  /* The calculus of Computation textbook */
+  def linearSearch(a: Array[Int], c: Int): Boolean = ({
+    require(a.length >= 0)
+    var i = 0
+    var found = false
+    (while(i < a.length) {
+      if(a(i) == c)
+        found = true
+      i = i + 1
+    }) invariant(
+         i <= a.length && 
+         i >= 0 && 
+         (if(found) contains(a, i, c) else !contains(a, i, c))
+       )
+    found
+  }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
+
+  def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+    require(a.length >= 0 && size >= 0 && size <= a.length)
+    content(a, size).contains(c)
+  }
+  
+  def content(a: Array[Int], size: Int): Set[Int] = {
+    require(a.length >= 0 && size >= 0 && size <= a.length)
+    var set = Set.empty[Int]
+    var i = 0
+    (while(i < size) {
+      set = set ++ Set(a(i))
+      i = i + 1
+    }) invariant(i >= 0 && i <= size)
+    set
+  }
+
+  def abs(tab: Array[Int]): Array[Int] = ({
+    require(tab.length >= 0)
+    var k = 0
+    val tabres = Array.fill(tab.length)(0)
+    (while(k < tab.length) {
+      if(tab(k) < 0)
+        tabres(k) = -tab(k)
+      else
+        tabres(k) = tab(k)
+      k = k + 1
+    }) invariant(
+        tabres.length == tab.length && 
+        k >= 0 && k <= tab.length && 
+        isPositive(tabres, k))
+    tabres
+  }) ensuring(res => isPositive(res, res.length))
+
+  def isPositive(a: Array[Int], size: Int): Boolean = {
+    require(a.length >= 0 && size <= a.length)
+    def rec(i: Int): Boolean = {
+      require(i >= 0)
+      if(i >= size) 
+        true 
+      else {
+        if(a(i) < 0) 
+          false 
+        else 
+          rec(i+1)
+      }
+    }
+    rec(0)
+  }
+
+  /* VSTTE 2010 challenge 1 */
+  def maxSum(a: Array[Int]): (Int, Int) = ({
+    require(a.length >= 0 && isPositive(a, a.length))
+    var sum = 0
+    var max = 0
+    var i = 0
+    (while(i < a.length) {
+      if(max < a(i)) 
+        max = a(i)
+      sum = sum + a(i)
+      i = i + 1
+    }) invariant (sum <= i * max && i >= 0 && i <= a.length)
+    (sum, max)
+  }) ensuring(res => res._1 <= a.length * res._2)
+
+}

testcases/master-thesis-regis/Constraints.scala

+import leon.Utils._
+
+object Epsilon4 {
+
+  sealed abstract class MyList
+  case class MyCons(head: Int, tail: MyList) extends MyList
+  case class MyNil() extends MyList
+
+  def size(lst: MyList): Int = (lst match {
+    case MyNil() => 0
+    case MyCons(_, xs) => 1 + size(xs)
+  })
+
+  def toSet(lst: MyList): Set[Int] = lst match {
+    case MyCons(x, xs) => toSet(xs) ++ Set(x)
+    case MyNil() => Set[Int]()
+  }
+
+  def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+    val elem = epsilon((x : Int) => set contains x)
+    MyCons(elem, toList(set -- Set[Int](elem)))
+  }
+
+  def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+}

testcases/master-thesis-regis/ListOperations.scala

+import leon.Utils._
+import leon.Annotations._
+
+object ListOperations {
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  sealed abstract class IPList
+  case class IPCons(head: (Int, Int), tail: IPList) extends IPList
+  case class IPNil() extends IPList
+
+  def content(l: List) : Set[Int] = l match {
+    case Nil() => Set.empty[Int]
+    case Cons(x, xs) => Set(x) ++ content(xs)
+  }
+
+  def iplContent(l: IPList) : Set[(Int, Int)] = l match {
+    case IPNil() => Set.empty[(Int, Int)]
+    case IPCons(x, xs) => Set(x) ++ iplContent(xs)
+  }
+
+  def size(l: List) : Int = {
+    var r = 0
+    var l2 = l
+    (while(!l2.isInstanceOf[Nil]) {
+      val Cons(_, tail) = l2
+      l2 = tail
+      r = r+1
+    }) invariant(r >= 0)
+    r
+  } ensuring(res => res >= 0)
+
+  def sizeBuggy(l: List) : Int = {
+    var r = -1
+    var l2 = l
+    (while(!l2.isInstanceOf[Nil]) {
+      val Cons(_, tail) = l2
+      l2 = tail
+      r = r+1
+    }) invariant(r >= 0)
+    r
+  } ensuring(res => res >= 0)
+
+  def sizeFun(l: List) : Int = l match {
+    case Nil() => 0
+    case Cons(_, t) => 1 + sizeFun(t)
+  } 
+
+  def iplSizeFun(l: IPList) : Int = l match {
+    case IPNil() => 0
+    case IPCons(_, t) => 1 + iplSizeFun(t)
+  }
+
+  def iplSize(l: IPList) : Int = {
+    var r = 0
+    var l2 = l
+    (while(!l2.isInstanceOf[IPNil]) {
+      val IPCons(_, tail) = l2
+      l2 = tail
+      r = r+1
+    }) invariant(r >= 0)
+    r
+  } ensuring(_ >= 0)
+
+  def sizeImpEqFun(l: List): Boolean = (size(l) == sizeFun(l)) ensuring(_ == true)
+
+  def zip(l1: List, l2: List) : IPList = ({
+    require(sizeFun(l1) == sizeFun(l2))
+    var  r: IPList = IPNil()
+    var ll1: List = l1
+    var ll2 = l2
+
+    (while(!ll1.isInstanceOf[Nil]) {
+      val Cons(l1head, l1tail) = ll1
+      val Cons(l2head, l2tail) = if(!ll2.isInstanceOf[Nil]) ll2 else Cons(0, Nil())
+      r = IPCons((l1head, l2head), r)
+      ll1 = l1tail
+      ll2 = l2tail
+    }) invariant(iplSizeFun(r) + sizeFun(ll1) == sizeFun(l1))
+
+    iplReverse(r)
+  }) ensuring(res => iplSizeFun(res) == sizeFun(l1))
+
+  def iplReverse(l: IPList): IPList = {
+    var r: IPList = IPNil()
+    var l2: IPList = l
+
+    (while(!l2.isInstanceOf[IPNil]) {
+      val IPCons(head, tail) = l2
+      l2 = tail
+      r = IPCons(head, r)
+    }) invariant(iplContent(r) ++ iplContent(l2) == iplContent(l) && iplSizeFun(r) + iplSizeFun(l2) == iplSizeFun(l))
+
+    r
+  } ensuring(res => iplContent(res) == iplContent(l) && iplSizeFun(res) == iplSizeFun(l))
+
+  def reverse(l: List): List = {
+    var r: List = Nil()
+    var l2: List = l
+
+    (while(!l2.isInstanceOf[Nil]) {
+      val Cons(head, tail) = l2
+      l2 = tail
+      r = Cons(head, r)
+    }) invariant(content(r) ++ content(l2) == content(l) && sizeFun(r) + sizeFun(l2) == sizeFun(l))
+
+    r
+  } ensuring(res => content(res) == content(l) && sizeFun(res) == sizeFun(l))
+
+  def listEqReverse(l: List): Boolean = {
+    l == reverse(l)
+  } ensuring(_ == true)
+
+  def append(l1 : List, l2 : List) : List = {
+    var r: List = l2
+    var tmp: List = reverse(l1)
+
+    (while(!tmp.isInstanceOf[Nil]) {
+      val Cons(head, tail) = tmp
+      tmp = tail
+      r = Cons(head, r)
+    }) invariant(content(r) ++ content(tmp) == content(l1) ++ content(l2))
+
+    r
+  } ensuring(content(_) == content(l1) ++ content(l2))
+
+  def appendBuggy(l1 : List, l2 : List) : List = {
+    var r: List = l2
+    var tmp: List = l1
+
+    while(!tmp.isInstanceOf[Nil]) {
+      val Cons(head, tail) = tmp
+      tmp = tail
+      r = Cons(head, r)
+    }
+
+    r
+  }
+
+  def appendEqAppendBuggy(l1: List, l2: List): Boolean = {
+    append(l1, l2) == appendBuggy(l1, l2)
+  } ensuring(_ == true)
+
+}