yay !

vstte10competition/SearchLinkedList.scala

@@ -12,38 +12,37 @@ object SearchLinkedList {
     case Cons(_, xs) => 1 + size(xs)
   }) ensuring(_ >= 0)
 
-  @induct
+  def contains(list : List, elem : Int) : Boolean = (list match {
+    case Nil() => false
+    case Cons(x, xs) => x == elem || contains(xs, elem)
+  })
+
   def firstZero(list : List) : Int = (list match {
     case Nil() => 0
     case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
-  }) ensuring (res => if (!contains(list, 0)) res == size(list) else zeroAt(list, res))
-
-  def zeroAt(list : List, pos : Int) : Boolean = {
-    require(pos >= 0)
-    list match {
-      case Nil() => false
-      case Cons(x, xs) => if (pos == 0) x == 0 else zeroAt(xs, pos - 1)
-    }
-  }
-
-  def prop0(list : List, pos : Int) : Boolean = {
-    require(pos >= 0)
-    list match {
-      case Nil() => true
-      case Cons(x, xs) => if (zeroAt(xs, pos)) zeroAt(list, pos + 1) else true
-    } 
-  } holds
+  }) ensuring (res =>
+    res >= 0 && (if (contains(list, 0)) {
+      firstZeroAtPos(list, res)
+    } else {
+      res == size(list)
+    }))
 
   def firstZeroAtPos(list : List, pos : Int) : Boolean = {
-    require(pos >= 0)
     list match {
       case Nil() => false
       case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
     }
-  } ensuring (res => if (res) contains(list, 0) else true)
+  } 
 
-  def contains(list : List, elem : Int) : Boolean = (list match {
-    case Nil() => false
-    case Cons(x, xs) => x == elem || contains(xs, elem)
-  })
+  def goal(list : List, i : Int) : Boolean = {
+    if(firstZero(list) == i) {
+      if(contains(list, 0)) {
+        firstZeroAtPos(list, i)
+      } else {
+        i == size(list)
+      }
+    } else {
+      true
+    }
+  } holds
 }