diff --git a/src/test/resources/regression/termination/valid/QuickSort.scala b/src/test/resources/regression/termination/valid/QuickSort.scala
index e356bdc2a2b8a1c412e90a3033ae269faf6d7df0..d4fb11ea68a7e8c96f056754c24be2e9a5f9ef4e 100644
--- a/src/test/resources/regression/termination/valid/QuickSort.scala
+++ b/src/test/resources/regression/termination/valid/QuickSort.scala
@@ -1,5 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.annotation._
import leon.lang._
object QuickSort {
@@ -29,7 +30,7 @@ object QuickSort {
case Nil() => bList
case _ => rev_append(reverse(aList),bList)
}
-
+
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
@@ -51,6 +52,7 @@ object QuickSort {
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
}) ensuring(res => contents(res) == contents(list)) // && is_sorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/src/test/resources/regression/termination/valid/SimpInterpret.scala b/src/test/resources/regression/termination/valid/SimpInterpret.scala
index 76fcd4145509440741b521bf26fa97dcc9af2dd9..c5255506dbb0b20308a0210ea3268a9432abaa14 100644
--- a/src/test/resources/regression/termination/valid/SimpInterpret.scala
+++ b/src/test/resources/regression/termination/valid/SimpInterpret.scala
@@ -1,15 +1,15 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-//import leon.annotation._
+import leon.annotation._
import leon.lang._
object Interpret {
- abstract class BoolTree
+ abstract class BoolTree
case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
case class Not(t : BoolTree) extends BoolTree
- abstract class IntTree
+ abstract class IntTree
case class Const(c:Int) extends IntTree
case class Var() extends IntTree
case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
@@ -22,7 +22,7 @@ object Interpret {
}
def beval(t:BoolTree, x0 : Int) : Boolean = {
- t match {
+ t match {
case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
@@ -62,6 +62,7 @@ object Interpret {
!treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
}.holds
+ @ignore
def main(args : Array[String]) {
thereIsGoodTree()
}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
index 05889fcb726ff88728959172f2127128831802c2..3252c9acf942d682f3cef10cc358cb7c837b44bb 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
@@ -34,7 +34,7 @@ object InsertionSort {
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 */
@@ -43,8 +43,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -54,11 +54,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index 7c89f364600e95edb8c0f266cb5e22f65d1adbea..0ec78ff0d3050b6333e3fd1e229dd57f2e72cea2 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -34,7 +34,7 @@ object InsertionSort {
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 */
@@ -43,8 +43,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -54,11 +54,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/repair/DaysToYears/DaysToYears.scala b/testcases/repair/DaysToYears/DaysToYears.scala
index bb6c518b3b743ea02d0188c8a9b1a802e6685e16..3a71a49602ff9d818df2cf2e1d2476a78f9e0b3a 100644
--- a/testcases/repair/DaysToYears/DaysToYears.scala
+++ b/testcases/repair/DaysToYears/DaysToYears.scala
@@ -1,10 +1,11 @@
+import leon.annotation._
import leon.lang._
object DaysToYears {
val base : Int = 1980
-
+
def isLeapYear(y : Int): Boolean = y % 4 == 0
-
+
def daysToYears(days : Int): Int = {
require(days > 0)
daysToYears1(base, days)._1
@@ -17,16 +18,17 @@ object DaysToYears {
else if (days > 365 && !isLeapYear(year))
daysToYears1(year + 1, days - 365)
else (year, days)
- } ensuring { res =>
+ } ensuring { res =>
res._2 <= 366 &&
- res._2 > 0 &&
+ res._2 > 0 &&
res._1 >= base &&
- (((year,days), res) passes {
+ (((year,days), res) passes {
case (1980, 366 ) => (1980, 366)
case (1980, 1000) => (1982, 269)
})
- }
+ }
+ @ignore
def main(args : Array[String]) = {
println(daysToYears1(base, 10593 ))
println(daysToYears1(base, 366 ))
diff --git a/testcases/repair/DaysToYears/DaysToYears1.scala b/testcases/repair/DaysToYears/DaysToYears1.scala
index 13eec09ae4ee1a611fc5a7d916ed92e061086112..1ef2d337989c7dc1a718637777d6e97726d7a276 100644
--- a/testcases/repair/DaysToYears/DaysToYears1.scala
+++ b/testcases/repair/DaysToYears/DaysToYears1.scala
@@ -1,10 +1,11 @@
+import leon.annotation._
import leon.lang._
object DaysToYears {
val base : Int = 1980
-
+
def isLeapYear(y : Int): Boolean = y % 4 == 0
-
+
def daysToYears(days : Int): Int = {
require(days > 0)
daysToYears1(base, days)._1
@@ -17,17 +18,18 @@ object DaysToYears {
else if (days > 365 && !isLeapYear(year))
daysToYears1(year, days - 365) // FIXME forgot +1
else (year, days)
- } ensuring { res =>
+ } ensuring { res =>
res._2 <= 366 &&
- res._2 > 0 &&
+ res._2 > 0 &&
res._1 >= base &&
- (((year,days), res) passes {
+ (((year,days), res) passes {
case (1999, 14 ) => (1999, 14)
case (1980, 366) => (1980, 366)
case (1981, 366) => (1982, 1)
})
- }
+ }
+ @ignore
def main(args : Array[String]) = {
println(daysToYears1(base, 10593 ))
println(daysToYears1(base, 366 ))
diff --git a/testcases/repair/DaysToYears/DaysToYears2.scala b/testcases/repair/DaysToYears/DaysToYears2.scala
index de0d31a707bda925004cca4dd3af1784995d0051..40396f05c6c3e40c4cfd0beccee02ed7d4c59553 100644
--- a/testcases/repair/DaysToYears/DaysToYears2.scala
+++ b/testcases/repair/DaysToYears/DaysToYears2.scala
@@ -1,10 +1,11 @@
+import leon.annotation._
import leon.lang._
object DaysToYears {
val base : Int = 1980
-
+
def isLeapYear(y : Int): Boolean = y % 4 == 0
-
+
def daysToYears(days : Int): Int = {
require(days > 0)
daysToYears1(base, days)._1
@@ -16,17 +17,18 @@ object DaysToYears {
daysToYears1(year + 1, days - 366) // TODO this branch cannot be solved although it is correct because it depends on the erroneous branch
else if (days > 365 && !isLeapYear(year))
daysToYears1(year + 1, days - 365)
- else (year + 1, days) // FIXME +1
- } ensuring { res =>
+ else (year + 1, days) // FIXME +1
+ } ensuring { res =>
res._2 <= 366 &&
- res._2 > 0 &&
+ res._2 > 0 &&
res._1 >= base &&
- (((year,days), res) passes {
+ (((year,days), res) passes {
case (1980, 366 ) => (1980, 366)
case (1980, 1000) => (1982, 269)
})
- }
+ }
+ @ignore
def main(args : Array[String]) = {
println(daysToYears1(base, 10593 ))
println(daysToYears1(base, 366 ))
diff --git a/testcases/runtime/SquareRoot.scala b/testcases/runtime/SquareRoot.scala
index 87b3e985a6209da18606c28ca189440043b6e25d..95bdf52f6c9e0967da3af474ba70cadc30e9cc45 100644
--- a/testcases/runtime/SquareRoot.scala
+++ b/testcases/runtime/SquareRoot.scala
@@ -1,3 +1,4 @@
+import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
@@ -23,6 +24,7 @@ object SquareRoot {
}
}
+ @ignore
def main(a: Array[String]) {
isqrt2(42)
}
diff --git a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
index 64a8ae73ddd8553ff4ca364814aa880c41b503f8..3cf66229cb37d2c00e41ab63d0fbe4fb28aa4945 100644
--- a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
+++ b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
@@ -1,3 +1,4 @@
+import leon.annotation._
import leon.lang._
import leon.collection._
@@ -50,7 +51,7 @@ object BatchedQueue {
case Cons(_, xs) => checkf(xs, p.r)
}
}
- //
+ //
// def last(p: Queue): Int = {
// require(!isEmpty(p))
// p.r match {
@@ -66,6 +67,7 @@ object BatchedQueue {
(if (isEmpty(p)) true
else content(tail(res)) ++ Set(x) == content(tail(res))))
+ @ignore
def main(args: Array[String]): Unit = {
val pair = Queue(Cons(4, Nil), Cons(3, Nil))
diff --git a/testcases/verification/case-studies/Robot3po.scala b/testcases/verification/case-studies/Robot3po.scala
index 56709fc5555175ede38fac4f00ec6e772ecb9d7d..b189db5e98852b61f9463232d1036a5fa519a8aa 100644
--- a/testcases/verification/case-studies/Robot3po.scala
+++ b/testcases/verification/case-studies/Robot3po.scala
@@ -365,7 +365,7 @@ object Robot {
}
def validState(rs: RobotState)(implicit w: World): Boolean = {
-
+
// 6) Sensors have consistent data
val recentData = rs.ns.validData && rs.hs.validData
@@ -509,6 +509,7 @@ object Robot {
}
+ @ignore
def main(a: Array[String]): Unit = {
val map0 = """|XXXXXXXXX
|XR FF X
diff --git a/testcases/verification/compilation/Interpreter.scala b/testcases/verification/compilation/Interpreter.scala
index 40dcab73cdb00b0b65dd960ca3e2427e4fa503c7..1c8e3bbde2b6dc18ba42211f2bfc498a0bcfaf71 100644
--- a/testcases/verification/compilation/Interpreter.scala
+++ b/testcases/verification/compilation/Interpreter.scala
@@ -1,12 +1,13 @@
+import leon.annotation._
import leon.lang._
object Interpret {
- abstract class BoolTree
+ abstract class BoolTree
case class Eq(t1 : IntTree, t2 : IntTree) extends BoolTree
case class And(t1 : BoolTree, t2 : BoolTree) extends BoolTree
case class Not(t : BoolTree) extends BoolTree
- abstract class IntTree
+ abstract class IntTree
case class Const(c:Int) extends IntTree
case class Var(index:Int) extends IntTree
case class Plus(t1 : IntTree, t2 : IntTree) extends IntTree
@@ -19,7 +20,7 @@ object Interpret {
}
def beval(t:BoolTree, x0 : Int) : Boolean = {
- t match {
+ t match {
case Less(t1, t2) => ieval(t1,x0) < ieval(t2,x0)
case Eq(t1, t2) => ieval(t1,x0) == ieval(t2,x0)
case And(t1, t2) => beval(t1,x0) && beval(t2,x0)
@@ -56,6 +57,7 @@ object Interpret {
!treeBad(If(Less(Const(0),Var(0)), Var(0), Minus(Const(0),Var(0))))
} holds
+ @ignore
def main(args : Array[String]) {
thereIsGoodTree()
}
diff --git a/testcases/verification/compilation/SimpInterpret.scala b/testcases/verification/compilation/SimpInterpret.scala
index fab5035897d86b4b587715cb4d7ef3459c1fed2f..6c61bad49173ecc0ff9edafc432d11eb6ffbbadb 100644
--- a/testcases/verification/compilation/SimpInterpret.scala
+++ b/testcases/verification/compilation/SimpInterpret.scala
@@ -1,5 +1,5 @@
//import scala.collection.immutable.Set
-//import leon.annotation._
+import leon.annotation._
import leon.lang._
object Interpret {
@@ -61,6 +61,7 @@ object Interpret {
!treeBad(If(Less(Const(0),Var()), Var(), Minus(Const(0),Var())))
} holds
+ @ignore
def main(args : Array[String]) {
thereIsGoodTree()
}
diff --git a/testcases/verification/graph/MST/MSTMap.scala b/testcases/verification/graph/MST/MSTMap.scala
index 1ef72da321d96c6b65977427c2aff485212c990e..e718256b6d226dea77efddadc970ffc44c7dab0f 100644
--- a/testcases/verification/graph/MST/MSTMap.scala
+++ b/testcases/verification/graph/MST/MSTMap.scala
@@ -15,16 +15,16 @@ object MSTMap {
def mst(g : Graph) : Map[(Int,Int), Int] = {
require(invariant(g) && isUndirected(g) && isConnected(g) &&
g.nVertices <= 3)
-
+
var uf_map = Map.empty[Int, Int] //map to represent parent
//relationship to model union find
var spanningTree = Map.empty[(Int,Int), Int]
var alreadyTested = Map.empty[(Int, Int), Int]
-
+
(while(!isConnected(spanningTree, g.nVertices)) {
val next_edge = getSmallestEdge(g.nVertices, g.edges, alreadyTested)
-
+
val p1 = uFind(next_edge._1, uf_map)
val p2 = uFind(next_edge._2, uf_map)
if(p1 != p2) {
@@ -45,18 +45,18 @@ object MSTMap {
// We only verify that the edge set returned corresponds to some
// spanning tree, but not that it is of minimal weight.
-
+
// Here, we always take the smallest edge regardless whether it
// creates a cycle or not,
// Leon loops
def mstBogus(g : Graph) : Map[(Int,Int), Int] = {
require(invariant(g) && isUndirected(g) && isConnected(g) &&
g.nVertices <= 4)
-
+
var edges = g.edges
var spanningTree = Map.empty[(Int,Int), Int]
var alreadyTested = Map.empty[(Int, Int), Int]
-
+
(while(!isConnected(spanningTree, g.nVertices)) {
val next_edge = getSmallestEdge(g.nVertices, edges, alreadyTested)
@@ -73,13 +73,13 @@ object MSTMap {
spanningTree
} ensuring(x => isAcyclic(x, g.nVertices) && isConnected(x, g.nVertices))
-
+
/*
-----------------------------------------------------------------------------
GRAPH FUNCTIONS
-----------------------------------------------------------------------------
*/
-
+
def invariant(g : Graph) = {
def noSelfLoops(i : Int) : Boolean = {
@@ -89,10 +89,10 @@ object MSTMap {
else
noSelfLoops(i+1)
}
-
+
g.nVertices >= 0 && noSelfLoops(0)
}
-
+
/**
Tests, if g is undirected, that is if for every edge (i,j) there is
also and edge (j,i)
@@ -108,11 +108,11 @@ object MSTMap {
var j = 0
while(j < g.nVertices && res) {
res = !edgeSet.isDefinedAt(i,j) || edgeSet.isDefinedAt(j,i)
-
+
//If weights should considered
if(res && edgeSet.isDefinedAt(i,j))
res = edgeSet(i,j) == edgeSet(j,i)
-
+
j += 1
}
i += 1
@@ -136,11 +136,11 @@ object MSTMap {
it this function would always return a valid edge, however, this
property is not easily expressible in Leon.
*/
-
+
var i = 0
val big = 100000000
var res = (-1,-1,big)
-
+
while(i < nVertices) {
var j = 0
while(j < nVertices) {
@@ -171,7 +171,7 @@ object MSTMap {
require(g.nVertices >= 0 && isUndirected(g))
isConnected(g.edges, g.nVertices)
}
-
+
def isConnected(edges : Map[(Int,Int), Int], nVertices : Int) : Boolean = {
require(nVertices >= 0)
val uf = calculateUF(edges, nVertices)._1
@@ -204,7 +204,7 @@ object MSTMap {
def calculateUF(edgeSet : Map[(Int,Int), Int], nVertices : Int) :
(Map[Int, Int], Boolean)= {
require(nVertices >= 0)
-
+
var i = 0
var uf = Map.empty[Int, Int]
var cycle = false
@@ -223,7 +223,7 @@ object MSTMap {
//"remove" twin edge
edges = edges.updated((j,i), -1)
- }
+ }
}
j += 1
}
@@ -232,7 +232,7 @@ object MSTMap {
(uf, cycle)
}
-
+
/* *************************************
Union find
*************************************** */
@@ -246,7 +246,7 @@ object MSTMap {
// naive union
val p1 = uFind(e1,s)
val p2 = uFind(e2, s)
-
+
if(p1 != p2)
//naive union
s.updated(p1, p2) //only union if theiy are really in different trees
@@ -257,7 +257,8 @@ object MSTMap {
// fsc -d classes -classpath
// ../../leon-2.0/target/scala-2.9.1-1/classes MST.scala
- // scala -classpath classes MST
+ // scala -classpath classes MST
+ @ignore
def main(args: Array[String]) {
val edges = Map((1,0) -> 10, (0,1) -> 10, (1,2) -> 12, (2,1) ->
12, (0,2) -> 18, (2,0) -> 18, (3,1) -> 20, (1,3) -> 20)
@@ -267,5 +268,5 @@ object MSTMap {
println(mst(g)); //works
println(mstBogus(g)); // crashes because postcondition doensn't hold
}
-
+
}
diff --git a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
index 4ac5d863e880a484a00a8fef939964607320e6db..b79751c692cf8ebcd7c2f24a85804dc210568a50 100644
--- a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
+++ b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala
@@ -11,14 +11,14 @@ object DijkstrasSortedList {
* Graph representation and algorithms
**************************************************************************/
case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
-
+
// Disallow self edges? Not actually important since they can be ignored.
def invariant(g : Graph) = g.nVertices >= 0
-
+
// true if x & y have same number of nodes and y has all x's edges
def isSubGraph(x : Graph, y : Graph) : Boolean = {
require(invariant(x) && invariant(y))
-
+
var ret : Boolean = (x.nVertices == y.nVertices)
if (ret){
var i = 0
@@ -34,11 +34,11 @@ object DijkstrasSortedList {
}
ret
}
-
+
// true if every edge has a weight of at least 0
def nonnegativeWeights(g : Graph) : Boolean = {
require(invariant(g))
-
+
var ret : Boolean = true
var i = 0
while(i<g.nVertices) {
@@ -54,20 +54,20 @@ object DijkstrasSortedList {
}
ret
}
-
+
// true if b is reachable from a
def isReachable(g : Graph, a : Int, b : Int) : Boolean = {
require(invariant(g) && a >= 0 && a < g.nVertices && b >= 0 && b < g.nVertices)
-
+
//TODO
false
}
-
-
+
+
/***************************************************************************
* Sorted list representation and algorithims
**************************************************************************/
-
+
/** A list containing node, dist pairs.
*
* Sorted by distance, nearest first. Distance must be non-negative. Node
@@ -76,7 +76,7 @@ object DijkstrasSortedList {
abstract class SortedNDList
case class ListNode(node : Int, dist : Int, next : SortedNDList) extends SortedNDList
case class ListEnd() extends SortedNDList
-
+
/** List invariant (see description above) */
@induct
def sndInvariant(list : SortedNDList) : Boolean = {
@@ -91,18 +91,18 @@ object DijkstrasSortedList {
false
case ListEnd() => true //len <= 3
}
-
+
invRec(list/*, Set.empty, 0, 0*/)
}
-
+
/** Look for node in list and remove, if it exists. */
@induct
def removeFromList(list : SortedNDList, node : Int) : SortedNDList ={
// something about this times out
require(sndInvariant(list))
-
+
//println("removeFromList: "+list)
-
+
list match {
case ListNode(n,d,next) =>
if (n == node)
@@ -113,7 +113,7 @@ object DijkstrasSortedList {
case ListEnd() => list
}
} ensuring(sndInvariant(_)) // something about this generates an error: is the precondition not checked for _all_ elements or something?
-
+
/** Return true if list contains node */
@induct
def listContains(list : SortedNDList, node : Int) : Boolean ={
@@ -126,14 +126,14 @@ object DijkstrasSortedList {
case ListEnd() => false
}
}
-
+
/** Add a new node to the list, such that list remains sorted by distance.
* Assume node is not already in list. */
@induct
def addSorted(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
// something to do with this times out
require(sndInvariant(list) && !listContains(list, node) && node >= 0 && dist >= 0)
-
+
list match {
case ListNode(n,d,next) =>
if (d > dist) // insert here
@@ -144,37 +144,37 @@ object DijkstrasSortedList {
ListNode(node, dist, list)
}
} ensuring (sndInvariant(_)) // something to do with this times out
-
+
/** Update node with distance minimum of dist and current value. Add if not
* in list, and maintain sorted order. */
@induct
def updateDistInList(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
require(sndInvariant(list) && node >= 0 && dist >= 0)
-
+
val listRemoved = removeFromList(list, node)
addSorted(listRemoved, node, dist)
} ensuring(sndInvariant(_))
-
-
+
+
/***************************************************************************
* Dijkstra's algorithm
**************************************************************************/
-
+
def isNodeNotB(list : SortedNDList, b : Int) : Boolean =
list match {
case ListNode(n, _, _) => n!=b
case ListEnd() => false
}
-
+
// common precondition: g is a valid graph and a and b are valid nodes
def bounds(g : Graph, a : Int, b : Int) : Boolean =
invariant(g) && 0 <= a && a < g.nVertices && 0 <= b && b < g.nVertices
-
+
// find the shortest path from a to b in g, and return its distance
// return -1 if the two aren't connected
def shortestPath(g : Graph, a : Int, b : Int) : Int = {
require(bounds(g,a,b) && nonnegativeWeights(g))
-
+
// We should always have at least some node if we haven't reached b (so
// long as b is in the graph and connected to a).
@induct
@@ -184,20 +184,20 @@ object DijkstrasSortedList {
* We should check same invariant at function exit. But there's no point:
* it's too much for Leon to reason about at once!
*/
-
+
list match {
case ListNode(node, dist, next) if (node==b) =>
list
case ListNode(node, dist, next) =>
var n = 0
var tail : SortedNDList = next
-
+
(while (n < g.nVertices){
if (n != node && !visited.contains(n) && g.edges.isDefinedAt((node,n)))
tail = updateDistInList(tail, n, dist+g.edges((node,n)))
n = n + 1
}) invariant(sndInvariant(list) && n >= 0 && n <= g.nVertices)
-
+
spVisit (tail, visited ++ Set(node))
case ListEnd() =>
list
@@ -206,7 +206,7 @@ object DijkstrasSortedList {
case ListEnd() => !isReachable(g,a,b)
case ListNode(node,_,_) => node==b
})
-
+
// We start from a, which has distance 0. All other nodes implicitly have
// infinite distance.
val startingList : SortedNDList = ListNode(a, 0, ListEnd())
@@ -221,12 +221,13 @@ object DijkstrasSortedList {
-1
}
} ensuring (res => res >= -1 /*(if (isReachable(g,a,b)) res>=0 else res== -1)*/)
-
+
+ @ignore
def main(args: Array[String]) {
val spanningTreeE = Map((0,1) -> 1, (0,2) -> 2, (2,3) -> 5, (0,3) -> 10, (3,2) -> 0)
val spanningTree = Graph(4, spanningTreeE)
val singleGraph = Graph(1, Map.empty)
-
+
println(spanningTree)
println("from 0 to 3 (should be 7): "+shortestPath(spanningTree,0,3))
println("from 3 to 1 (no path): "+shortestPath(spanningTree,3,1))
diff --git a/testcases/verification/list-algorithms/InsertionSort.scala b/testcases/verification/list-algorithms/InsertionSort.scala
index 35062e263c1a9b869bf2c34a25196ae4fbce3811..980927204dad1e609e93dd8dcf8a364d027e113d 100644
--- a/testcases/verification/list-algorithms/InsertionSort.scala
+++ b/testcases/verification/list-algorithms/InsertionSort.scala
@@ -51,7 +51,7 @@ object InsertionSort {
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 */
@@ -60,8 +60,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -73,8 +73,8 @@ object InsertionSort {
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)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -84,11 +84,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/verification/list-algorithms/MergeSort.scala b/testcases/verification/list-algorithms/MergeSort.scala
index 1bbd7f607528a9549363dec4d3e73f547f602565..5fc80d117c9eae3bddec01377683eac54f0c37cd 100644
--- a/testcases/verification/list-algorithms/MergeSort.scala
+++ b/testcases/verification/list-algorithms/MergeSort.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.annotation._
object MergeSort {
sealed abstract class List
@@ -57,6 +58,7 @@ object MergeSort {
}) ensuring(res => contents(res) == contents(list) && is_sorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
println(ls)
diff --git a/testcases/verification/list-algorithms/QuickSort.scala b/testcases/verification/list-algorithms/QuickSort.scala
index 30b3621438bd0ef944b61f831b36379deb1470f6..1afbc3a2b4d7c5f5a54560a6aa401d396646390c 100644
--- a/testcases/verification/list-algorithms/QuickSort.scala
+++ b/testcases/verification/list-algorithms/QuickSort.scala
@@ -53,7 +53,7 @@ object QuickSort {
case Nil() => bList
case _ => rev_append(reverse(aList),bList)
}) ensuring(content(_) == content(aList) ++ content(bList))
-
+
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
@@ -69,7 +69,7 @@ object QuickSort {
case Nil() => Nil()
case Cons(x,xs) => if (n>x) Cons(x,smaller(n,xs)) else smaller(n,xs)
}
-
+
@induct
def smallerProp(n: Int, list: List): Boolean = (max(smaller(n, list)) match {
case Some(m) => n > m
@@ -117,6 +117,7 @@ object QuickSort {
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
}) ensuring(res => content(res) == content(list)) // && isSorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/verification/math/Prime.scala b/testcases/verification/math/Prime.scala
index d8de43f86cf8ec2528e54125dc42148f4cc49e84..1e928dcff5af0eb281f2b192bdd0a88a4cbe0fb5 100644
--- a/testcases/verification/math/Prime.scala
+++ b/testcases/verification/math/Prime.scala
@@ -1,3 +1,5 @@
+import leon.annotation._
+
object Prime {
// an attempt at defining isPrime in PureScala...
@@ -36,6 +38,7 @@ object Prime {
} ensuring(res => !res)
// Just for testing.
+ @ignore
def main(args : Array[String]) : Unit = {
def test(n : BigInt) : Unit = {
println("Is " + n + " prime ? -> " + isPrime(n))
diff --git a/testcases/verification/xlang/InsertionSort.scala b/testcases/verification/xlang/InsertionSort.scala
index 0a53cb55f4ef32b775646e1ea43a8c74b33a80c7..71dab126cda6927380c9395b39dcc49f3a550801 100644
--- a/testcases/verification/xlang/InsertionSort.scala
+++ b/testcases/verification/xlang/InsertionSort.scala
@@ -32,7 +32,7 @@ object InsertionSort {
case Nil() => true
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
- }
+ }
def isReversedSorted(l: List): Boolean = l match {
case Nil() => true
case Cons(x, Nil()) => true
@@ -66,8 +66,8 @@ object InsertionSort {
l match {
case Nil() => Cons(e,Nil())
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -79,8 +79,8 @@ object InsertionSort {
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)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -90,11 +90,12 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/web/demos/008_Tutorial-Robot.scala b/testcases/web/demos/008_Tutorial-Robot.scala
index c78dc15f2c48703bae470cd41578c7b141d7d9ee..bca1f367a26df843e65cea76de7029652f0b4906 100644
--- a/testcases/web/demos/008_Tutorial-Robot.scala
+++ b/testcases/web/demos/008_Tutorial-Robot.scala
@@ -365,7 +365,7 @@ object Robot {
}
def validState(rs: RobotState)(implicit w: World): Boolean = {
-
+
// 6) Sensors have consistent data
val recentData = rs.ns.validData && rs.hs.validData
@@ -509,6 +509,7 @@ object Robot {
}
+ @ignore
def main(a: Array[String]): Unit = {
val map0 = """|XXXXXXXXX
|XR FF X
diff --git a/testcases/web/verification/03_Insertion_Sort.scala b/testcases/web/verification/03_Insertion_Sort.scala
index e53b89b1732bed1dfb1c1389feacc70d4490285d..4b1c8ef7cd0b61ab0c2f91533598be792dd1b809 100644
--- a/testcases/web/verification/03_Insertion_Sort.scala
+++ b/testcases/web/verification/03_Insertion_Sort.scala
@@ -24,7 +24,7 @@ object InsertionSort {
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 */
@@ -33,8 +33,8 @@ object InsertionSort {
l match {
case Nil => Cons(e,Nil)
case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }
- } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -44,8 +44,8 @@ object InsertionSort {
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)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
&& isSorted(res)
&& size(res) == size(l) + 1
)
@@ -55,7 +55,7 @@ object InsertionSort {
def sort(l: List): List = (l match {
case Nil => Nil
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l)
+ }) ensuring(res => contents(res) == contents(l)
&& isSorted(res)
&& size(res) == size(l)
)
@@ -69,6 +69,7 @@ object InsertionSort {
}
} ensuring(res => contents(res) == contents(l1) ++ contents(l2) && isSorted(res))
+ @ignore
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil))))))