cleaner examples

mytest/Abs.scala

@@ -18,25 +18,34 @@ object Abs {
   }) ensuring(res => isArray(res, size) && isPositive(res, size))
 
   def isPositive(a: Map[Int, Int], size: Int): Boolean = {
-    require(isArray(a, size))
-    def rec(i: Int): Boolean = if(i >= size) true else {
-      if(a(i) < 0) false else rec(i+1)
+    require(size <= 10 && isArray(a, size))
+    def rec(i: Int): Boolean = {
+      require(i >= 0)
+      if(i >= size) 
+        true 
+      else {
+        if(a(i) < 0) 
+          false 
+        else 
+          rec(i+1)
+      }
     }
     rec(0)
   }
 
   def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+    def rec(i: Int): Boolean = {
+      require(i >= 0)  
+      if(i >= size) true else {
+        if(a.isDefinedAt(i)) rec(i+1) else false
+      }
+    }
+
     if(size < 0)
       false
     else
-      rec(a, size, 0)
-  }
-
-  def rec(a: Map[Int, Int], size: Int, i: Int): Boolean = {
-    require(i >= 0 && i <= size)
-    if(i >= size) true else { 
-      if(a.isDefinedAt(i)) rec(a, size, i+1) else false
-    }
+      rec(0)
   }
 
 }

mytest/Bubble.scala

@@ -34,7 +34,7 @@ object Bubble {
   }) ensuring(res => sorted(res, size, 0, size-1))
 
   def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
-    require(isArray(a, size) && l >= 0 && u < size && l <= u)
+    require(isArray(a, size) && size < 5 && l >= 0 && u < size && l <= u)
     var k = l
     var isSorted = true
     while(k <= u) {
@@ -46,27 +46,30 @@ object Bubble {
   }
   
   def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
-    require(l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && isArray(a, size))
+    require(l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && isArray(a, size) && size < 5)
     var i = l1
     var j = l2
     var isPartitionned = true
-    while(i <= u1) {
-      while(j <= u2) {
+    (while(i <= u1) {
+      j = l2
+      (while(j <= u2) {
         if(a(i) > a(j))
           isPartitionned = false
         j = j+1
-      }
+      }) invariant(j >= l2 && j+1 <= u2)
       i = i + 1
-    }
+    }) invariant(i >= l1 && i+1 <= u1)
     isPartitionned
   }
 
-
   def isArray(a: Map[Int, Int], size: Int): Boolean = {
     def rec(i: Int): Boolean = if(i >= size) true else {
       if(a.isDefinedAt(i)) rec(i+1) else false
     }
-    size > 0 && rec(0)
+    if(size <= 0)
+      false
+    else
+      rec(0)
   }
 
 }

mytest/LinearSearch.scala

@@ -2,16 +2,50 @@ import leon.Utils._
 
 object LinearSearch {
 
-  def linearSearch(a: Map[Int, Int], size: Int, c: Int, j: Int): Boolean = ({
-    require(size > 0 && j >= 0 && j < size)
+  def linearSearch(a: Map[Int, Int], size: Int, c: Int): Boolean = ({
+    require(size <= 5 && isArray(a, size))
     var i = 0
     var found = false
     (while(i < size) {
       if(a(i) == c)
         found = true
       i = i + 1
-    }) invariant((if(j < i && !found) a(j) != c else true))
+    }) invariant(i <= size && 
+                 i >= 0 && 
+                 (if(found) contains(a, i, c) else !contains(a, i, c))
+                )
     found
-  }) ensuring(res => (if(!res) a(j) != c else true))
+  }) ensuring(res => if(res) contains(a, size, c) else !contains(a, size, c))
 
+  def contains(a: Map[Int, Int], size: Int, c: Int): Boolean = {
+    require(isArray(a, size) && size <= 5)
+    content(a, size).contains(c)
+  }
+  
+
+  def content(a: Map[Int, Int], size: Int): Set[Int] = {
+    require(isArray(a, size) && size <= 5)
+    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 isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+    def rec(i: Int): Boolean = {
+      require(i >= 0)  
+      if(i >= size) true else {
+        if(a.isDefinedAt(i)) rec(i+1) else false
+      }
+    }
+
+    if(size < 0)
+      false
+    else
+      rec(0)
+  }
 }

src/main/scala/leon/plugin/CodeExtraction.scala

@@ -376,8 +376,31 @@ trait CodeExtraction extends Extractors {
       var reqCont: Option[Expr] = None
       var ensCont: Option[Expr] = None
       
+      realBody match {
+        case ExEnsuredExpression(body2, resSym, contract) => {
+          varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
+          val c1 = scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies) (contract)
+          // varSubsts.remove(resSym)
+          realBody = body2
+          ensCont = Some(c1)
+        }
+        case ExHoldsExpression(body2) => {
+          realBody = body2
+          ensCont = Some(ResultVariable().setType(BooleanType))
+        }
+        case _ => ;
+      }
+
+      realBody match {
+        case ExRequiredExpression(body3, contract) => {
+          realBody = body3
+          reqCont = Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies) (contract))
+        }
+        case _ => ;
+      }
+      
       val bodyAttempt = try {
-        Some(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody))
+        Some(flattenBlocks(scala2PureScala(unit, pluginInstance.silentlyTolerateNonPureBodies)(realBody)))
       } catch {
         case e: ImpureCodeEncounteredException => None
       }