diff --git a/src/test/resources/regression/testcases b/src/test/resources/regression/testcases new file mode 120000 index 0000000000000000000000000000000000000000..a8cc08a502f72dd81dfda87cb64f3f6d6472d8a5 --- /dev/null +++ b/src/test/resources/regression/testcases @@ -0,0 +1 @@ +../../../../testcases/ \ No newline at end of file diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala index c43e597a61aced0c3a4708d0c9189ee8c91a7ab0..c5e3c7f4087e9f32e25904c542861799285c2da9 100644 --- a/src/test/scala/leon/test/LeonTestSuite.scala +++ b/src/test/scala/leon/test/LeonTestSuite.scala @@ -152,7 +152,17 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach { - def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = { + def scanFilesIn(f: File, filter: String=>Boolean = all, recursive: Boolean = false): Iterable[File] = { + f.listFiles().flatMap{f => + if (f.isDirectory && recursive) { + scanFilesIn(f, filter, recursive) + } else { + List(f) + } + }.filter(f => filter(f.getPath)) + } + + def filesInResourceDir(dir : String, filter : String=>Boolean = all, recursive: Boolean = false) : Iterable[File] = { val d = this.getClass.getClassLoader.getResource(dir) @@ -161,6 +171,6 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach { new File(resourceDirHard + dir) } else new File(d.toURI) - asFile.listFiles().filter(f => filter(f.getPath)) + scanFilesIn(asFile, filter, recursive) } } diff --git a/src/test/scala/leon/test/LeonTests.scala b/src/test/scala/leon/test/LeonTests.scala index d7db5f39e69760f7a434988a54a6e9ba2ffccd8d..5650ab907d484b2e521e5dd4f256eec341132ebd 100644 --- a/src/test/scala/leon/test/LeonTests.scala +++ b/src/test/scala/leon/test/LeonTests.scala @@ -30,9 +30,12 @@ class LeonFunTests extends Suites( new SynthesisSuite, new SynthesisRegressionSuite, + new LibraryVerificationRegression, new PureScalaVerificationRegression, - new XLangVerificationRegression + new XLangVerificationRegression, + + new TestCasesCompile ) class LeonUnitTests extends Suites( diff --git a/src/test/scala/leon/test/testcases/TestCasesCompile.scala b/src/test/scala/leon/test/testcases/TestCasesCompile.scala new file mode 100644 index 0000000000000000000000000000000000000000..c6aad47dbb439be9714c36136997fdf43d379c8d --- /dev/null +++ b/src/test/scala/leon/test/testcases/TestCasesCompile.scala @@ -0,0 +1,53 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + +package leon.test.frontends + +import leon._ +import test.LeonTestSuite +import purescala.Definitions.Program +import java.io.File + +class TestCasesCompile extends LeonTestSuite { + // Hard-code output directory, for Eclipse purposes + + val pipeline = frontends.scalac.ExtractionPhase andThen utils.PreprocessingPhase + + def testFrontend(f: File, strip: Int) = { + val name = f.getAbsolutePath.split("/").toList.drop(strip).mkString("/") + + test("Compiling testcase " + name) { + val ctx = createLeonContext() + try { + pipeline.run(ctx)(List(f.getAbsolutePath)) + } catch { + case _: LeonFatalError => + fail("Failed to compile.") + } + } + } + + private def forEachFileIn(path : String)(block : File => Unit) { + val fs = filesInResourceDir(path, _.endsWith(".scala"), recursive=true) + + for(f <- fs.toSeq.sortBy(_.getAbsolutePath)) { + block(f) + } + } + + val baseDir = "regression/testcases/" + + val slashes = resourceDir(baseDir).getAbsolutePath.split("/").toList.size + + forEachFileIn(baseDir+"repair/") { f => + testFrontend(f, slashes) + } + forEachFileIn(baseDir+"runtime/") { f => + testFrontend(f, slashes) + } + forEachFileIn(baseDir+"synthesis/") { f => + testFrontend(f, slashes) + } + forEachFileIn(baseDir+"verification/") { f => + testFrontend(f, slashes) + } +} diff --git a/testcases/synthesis/insynth-leon-tests/BubbleSortBug.scala b/testcases/graveyard/insynth-leon-tests/BubbleSortBug.scala similarity index 100% rename from testcases/synthesis/insynth-leon-tests/BubbleSortBug.scala rename to testcases/graveyard/insynth-leon-tests/BubbleSortBug.scala diff --git a/testcases/synthesis/insynth-leon-tests/CaseClassSelectExample.scala b/testcases/graveyard/insynth-leon-tests/CaseClassSelectExample.scala similarity index 100% rename from testcases/synthesis/insynth-leon-tests/CaseClassSelectExample.scala rename to testcases/graveyard/insynth-leon-tests/CaseClassSelectExample.scala diff --git a/testcases/synthesis/insynth-leon-tests/Hole.scala b/testcases/graveyard/insynth-leon-tests/Hole.scala similarity index 100% rename from testcases/synthesis/insynth-leon-tests/Hole.scala rename to testcases/graveyard/insynth-leon-tests/Hole.scala diff --git a/testcases/synthesis/insynth-leon-tests/ListOperationsHole.scala b/testcases/graveyard/insynth-leon-tests/ListOperationsHole.scala similarity index 100% rename from testcases/synthesis/insynth-leon-tests/ListOperationsHole.scala rename to testcases/graveyard/insynth-leon-tests/ListOperationsHole.scala diff --git a/testcases/synthesis/insynth-leon-tests/RedBlackTreeFull.scala b/testcases/graveyard/insynth-leon-tests/RedBlackTreeFull.scala similarity index 100% rename from testcases/synthesis/insynth-leon-tests/RedBlackTreeFull.scala rename to testcases/graveyard/insynth-leon-tests/RedBlackTreeFull.scala diff --git a/testcases/synthesis/insynth-synthesis-tests/Hole.scala b/testcases/graveyard/insynth-synthesis-tests/Hole.scala similarity index 100% rename from testcases/synthesis/insynth-synthesis-tests/Hole.scala rename to testcases/graveyard/insynth-synthesis-tests/Hole.scala diff --git a/testcases/synthesis/insynth-synthesis-tests/LocalScope.scala b/testcases/graveyard/insynth-synthesis-tests/LocalScope.scala similarity index 100% rename from testcases/synthesis/insynth-synthesis-tests/LocalScope.scala rename to testcases/graveyard/insynth-synthesis-tests/LocalScope.scala diff --git a/testcases/verification/graph/MST/SpanningTree.scala b/testcases/graveyard/verification/graph/MST/SpanningTree.scala similarity index 99% rename from testcases/verification/graph/MST/SpanningTree.scala rename to testcases/graveyard/verification/graph/MST/SpanningTree.scala index 0b564b62dc74d41e14d7088f4a80aa3f6e2b0f44..3d421f6dc46c5dd8e77a9e38c5de603ff1d0b356 100644 --- a/testcases/verification/graph/MST/SpanningTree.scala +++ b/testcases/graveyard/verification/graph/MST/SpanningTree.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/SetIteration.scala b/testcases/graveyard/verification/graph/SetIteration.scala similarity index 98% rename from testcases/verification/graph/SetIteration.scala rename to testcases/graveyard/verification/graph/SetIteration.scala index f272a48a433cd7748ac9fbb551c6d5c81539f2e4..47eb20aa7067aa8ac45a15190ebdf979175be85b 100644 --- a/testcases/verification/graph/SetIteration.scala +++ b/testcases/graveyard/verification/graph/SetIteration.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/dijkstras/DijkstrasSet.scala b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSet.scala similarity index 99% rename from testcases/verification/graph/dijkstras/DijkstrasSet.scala rename to testcases/graveyard/verification/graph/dijkstras/DijkstrasSet.scala index 711eff7459e83fcce4e6e86c3ec49a8454b36ce4..96571c95f46a39f2d06abcfc3547f6587a67eee7 100644 --- a/testcases/verification/graph/dijkstras/DijkstrasSet.scala +++ b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSet.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSetToVisit.scala similarity index 99% rename from testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala rename to testcases/graveyard/verification/graph/dijkstras/DijkstrasSetToVisit.scala index eb954e7caaec7356fbf1598abc5704dea1b4932c..3664d99da6e04a8c1ad916d5dc0493e8b4f60b75 100644 --- a/testcases/verification/graph/dijkstras/DijkstrasSetToVisit.scala +++ b/testcases/graveyard/verification/graph/dijkstras/DijkstrasSetToVisit.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/vmcai2011-testcases/CADE07.scala b/testcases/graveyard/verification/vmcai2011-testcases/CADE07.scala similarity index 99% rename from testcases/verification/vmcai2011-testcases/CADE07.scala rename to testcases/graveyard/verification/vmcai2011-testcases/CADE07.scala index e1e6971405848cfb95ee3208ef6a9973f5b7a9f7..0af2fdd4980d2051fa6a5a34950fe236546b1bb4 100644 --- a/testcases/verification/vmcai2011-testcases/CADE07.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/CADE07.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object CADE07 { def vc1(listContent: Set[Int]) : Boolean = { diff --git a/testcases/verification/vmcai2011-testcases/CADE07Hard.scala b/testcases/graveyard/verification/vmcai2011-testcases/CADE07Hard.scala similarity index 99% rename from testcases/verification/vmcai2011-testcases/CADE07Hard.scala rename to testcases/graveyard/verification/vmcai2011-testcases/CADE07Hard.scala index 9b4206bdcae94e1960ecece6040c023becbc0f0d..e6e9aa0622465ad1eb4a5437d814ed8fedad2466 100644 --- a/testcases/verification/vmcai2011-testcases/CADE07Hard.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/CADE07Hard.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object CADE07Hard { def vc6a(l1 : Int, nul : Int, ths : Int, tmp357 : Int, list : Set[Int], objct : Set[Int], objAlloc : Set[Int], objAlloc16 : Set[Int], objAlloc30 : Set[Int], objAlloc45 : Set[Int], objAlloc60 : Set[Int], objAlloc74 : Set[Int], listContent : Set[Int], listContent59 : Set[Int], listContent73 : Set[Int], s241 : Set[Int], s142 : Set[Int], tmp171 : Boolean) : Set[Int] = { diff --git a/testcases/verification/vmcai2011-testcases/Giuliano.scala b/testcases/graveyard/verification/vmcai2011-testcases/Giuliano.scala similarity index 95% rename from testcases/verification/vmcai2011-testcases/Giuliano.scala rename to testcases/graveyard/verification/vmcai2011-testcases/Giuliano.scala index 51ed40b0a5a52a68092114962f00aa6649c2d65d..b69f0948506235e380c2ead20b688adddce93b25 100644 --- a/testcases/verification/vmcai2011-testcases/Giuliano.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/Giuliano.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object Giuliano { sealed abstract class List diff --git a/testcases/verification/vmcai2011-testcases/JustFormulas.scala b/testcases/graveyard/verification/vmcai2011-testcases/JustFormulas.scala similarity index 98% rename from testcases/verification/vmcai2011-testcases/JustFormulas.scala rename to testcases/graveyard/verification/vmcai2011-testcases/JustFormulas.scala index bb902f0d5734d47a86062f2f56d0f6cc162af59f..f8c9b84a011e9cae15c799b03739a5815ce428d8 100644 --- a/testcases/verification/vmcai2011-testcases/JustFormulas.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/JustFormulas.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object JustFormulas { // These are just to provide some "uninterpreted function symbols" diff --git a/testcases/verification/vmcai2011-testcases/ListProperties.scala b/testcases/graveyard/verification/vmcai2011-testcases/ListProperties.scala similarity index 98% rename from testcases/verification/vmcai2011-testcases/ListProperties.scala rename to testcases/graveyard/verification/vmcai2011-testcases/ListProperties.scala index 45b2ad1e1746a64efe448399eec8f785ba408b97..aaa830d37894bf0a8979d76dc6690351a813d11c 100644 --- a/testcases/verification/vmcai2011-testcases/ListProperties.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/ListProperties.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object IntListProperties { sealed abstract class IntList diff --git a/testcases/verification/vmcai2011-testcases/PaperExamples.scala b/testcases/graveyard/verification/vmcai2011-testcases/PaperExamples.scala similarity index 96% rename from testcases/verification/vmcai2011-testcases/PaperExamples.scala rename to testcases/graveyard/verification/vmcai2011-testcases/PaperExamples.scala index 5f5329fb8a4b468dc6bb94ad60c211408aff7ed4..9ee07e0b4c58ef77a7a76b7aab26493f210612f4 100644 --- a/testcases/verification/vmcai2011-testcases/PaperExamples.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/PaperExamples.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object PaperExamples { sealed abstract class List diff --git a/testcases/verification/vmcai2011-testcases/SanityChecks.scala b/testcases/graveyard/verification/vmcai2011-testcases/SanityChecks.scala similarity index 98% rename from testcases/verification/vmcai2011-testcases/SanityChecks.scala rename to testcases/graveyard/verification/vmcai2011-testcases/SanityChecks.scala index 5ee5f3d962e4629974ee2c94b37bca4002f9f7c8..df1f6582ce55368da4bc0d59a3c4b62410e33154 100644 --- a/testcases/verification/vmcai2011-testcases/SanityChecks.scala +++ b/testcases/graveyard/verification/vmcai2011-testcases/SanityChecks.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object SanityChecks { // These are just to provide some "uninterpreted function symbols" diff --git a/testcases/verification/xlang/BubbleSort.scala b/testcases/graveyard/verification/xlang/BubbleSort.scala similarity index 100% rename from testcases/verification/xlang/BubbleSort.scala rename to testcases/graveyard/verification/xlang/BubbleSort.scala diff --git a/testcases/verification/xlang/NonDeterministicList.scala b/testcases/graveyard/verification/xlang/NonDeterministicList.scala similarity index 100% rename from testcases/verification/xlang/NonDeterministicList.scala rename to testcases/graveyard/verification/xlang/NonDeterministicList.scala diff --git a/testcases/verification/xlang/QuickSortImp.scala b/testcases/graveyard/verification/xlang/QuickSortImp.scala similarity index 100% rename from testcases/verification/xlang/QuickSortImp.scala rename to testcases/graveyard/verification/xlang/QuickSortImp.scala diff --git a/testcases/verification/xlang/buggyEpsilon.scala b/testcases/graveyard/verification/xlang/buggyEpsilon.scala similarity index 100% rename from testcases/verification/xlang/buggyEpsilon.scala rename to testcases/graveyard/verification/xlang/buggyEpsilon.scala diff --git a/testcases/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala b/testcases/graveyard/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala similarity index 100% rename from testcases/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala rename to testcases/graveyard/verification/xlang/master-thesis-regis/ArrayBubbleSort.scala diff --git a/testcases/verification/xlang/master-thesis-regis/ArrayOperations.scala b/testcases/graveyard/verification/xlang/master-thesis-regis/ArrayOperations.scala similarity index 100% rename from testcases/verification/xlang/master-thesis-regis/ArrayOperations.scala rename to testcases/graveyard/verification/xlang/master-thesis-regis/ArrayOperations.scala diff --git a/testcases/verification/xlang/master-thesis-regis/Constraints.scala b/testcases/graveyard/verification/xlang/master-thesis-regis/Constraints.scala similarity index 100% rename from testcases/verification/xlang/master-thesis-regis/Constraints.scala rename to testcases/graveyard/verification/xlang/master-thesis-regis/Constraints.scala diff --git a/testcases/verification/xlang/xplusone.scala b/testcases/graveyard/verification/xlang/xplusone.scala similarity index 100% rename from testcases/verification/xlang/xplusone.scala rename to testcases/graveyard/verification/xlang/xplusone.scala diff --git a/testcases/repair/Heap/Heap.scala b/testcases/repair/Heap/Heap.scala index 5ceed2228715ceb2ea9bb7270c81c3608698a6a9..46be0f31a1a0855d31ed4b0ec929aa3d7cb5a49a 100644 --- a/testcases/repair/Heap/Heap.scala +++ b/testcases/repair/Heap/Heap.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap1.scala b/testcases/repair/Heap/Heap1.scala index b5d5b22d0d81b2917dd91ac82677d97d6fb45c24..61ec4ac0fb67a268daab399c43036270054b695e 100644 --- a/testcases/repair/Heap/Heap1.scala +++ b/testcases/repair/Heap/Heap1.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap10.scala b/testcases/repair/Heap/Heap10.scala index 27a75d344f8c4d7afb944b0cd7b07bbfd4e57587..6847ed8cd4635d58ee259c03f60de701703a2266 100644 --- a/testcases/repair/Heap/Heap10.scala +++ b/testcases/repair/Heap/Heap10.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap2.scala b/testcases/repair/Heap/Heap2.scala index df7e824580e82ea1bafd687abecc649892acfad9..914fb0971f6ee70f3362eb45d1dab82d26d4a6ba 100644 --- a/testcases/repair/Heap/Heap2.scala +++ b/testcases/repair/Heap/Heap2.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala index ebe8c85f20027db62dbec9f2b9740efec53393d7..2adde538b7c8a303865ab5532f64510fbbdfdb9c 100644 --- a/testcases/repair/Heap/Heap3.scala +++ b/testcases/repair/Heap/Heap3.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap4.scala b/testcases/repair/Heap/Heap4.scala index a19ff6c208acc587d355d8e7c311eb4a059fb3b3..ff78b370006c55798e74a13712fa921cf2b79e95 100644 --- a/testcases/repair/Heap/Heap4.scala +++ b/testcases/repair/Heap/Heap4.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap5.scala b/testcases/repair/Heap/Heap5.scala index 33a3ff5aac56c67109ecd2f9a242c27e41fc69fa..17777f85c6662c35cb61465253c350957f8fdbb5 100644 --- a/testcases/repair/Heap/Heap5.scala +++ b/testcases/repair/Heap/Heap5.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap6.scala b/testcases/repair/Heap/Heap6.scala index c9bf9d61ac83bb507d7300b89d7bb1c92e275e4c..a434b70c85cb3e94d103b7f7229db786898a4caf 100644 --- a/testcases/repair/Heap/Heap6.scala +++ b/testcases/repair/Heap/Heap6.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap7.scala b/testcases/repair/Heap/Heap7.scala index d4de52fe4dde4a0af4562b2bd047c5ee0a794c9c..9de2a20b68be2e7df30435bb8922bd4e42552f85 100644 --- a/testcases/repair/Heap/Heap7.scala +++ b/testcases/repair/Heap/Heap7.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap8.scala b/testcases/repair/Heap/Heap8.scala index 83a75b7ae9dca9d0e2068a69363de7b85fa6f18f..6ee493600578e8d179baeea2c21b81cc2f8b4949 100644 --- a/testcases/repair/Heap/Heap8.scala +++ b/testcases/repair/Heap/Heap8.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/Heap/Heap9.scala b/testcases/repair/Heap/Heap9.scala index 6846a9cae6fd0f37f2601c118fb6a502abe61c37..55520379ebb4473658818c7694abf4611971b059 100644 --- a/testcases/repair/Heap/Heap9.scala +++ b/testcases/repair/Heap/Heap9.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/repair/List/List.scala b/testcases/repair/List/List.scala index 19cf5ed3f4d734eb8dae19d0ffd26256cbadd969..caa4aa0d34678b0e282b2694191cc640cd466fc3 100644 --- a/testcases/repair/List/List.scala +++ b/testcases/repair/List/List.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala index 1e18ca898e18e18062da7189bd25093e7dc42311..9f600f7282660ccf581aa0050e62e3bcb3aac622 100644 --- a/testcases/repair/List/List1.scala +++ b/testcases/repair/List/List1.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List10.scala b/testcases/repair/List/List10.scala index 6ef82201bcb2a13867f4ab2b489da394966d3dcc..1c4b0016aead23b3ce26f1c018385e8812f396f6 100644 --- a/testcases/repair/List/List10.scala +++ b/testcases/repair/List/List10.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List11.scala b/testcases/repair/List/List11.scala index ce946496e175cedf92a8761fd2b3ea124e47e28b..7fe816b465e70afe6522ef75754c274f12c22784 100644 --- a/testcases/repair/List/List11.scala +++ b/testcases/repair/List/List11.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List12.scala b/testcases/repair/List/List12.scala index 63c1da6be5c444b13525c444dfb207ce1b976c5c..19f2d779e227d5b2daa52e3fc77b1310583ade23 100644 --- a/testcases/repair/List/List12.scala +++ b/testcases/repair/List/List12.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala index 4dc3f2177b30344665d1bb8fb34da38d77b31d17..b585f3ef1027c4e69c55495b3b904e485079f044 100644 --- a/testcases/repair/List/List13.scala +++ b/testcases/repair/List/List13.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List2.scala b/testcases/repair/List/List2.scala index 5a000adc8b1a9fb326150e9a948466d85e8f5991..f83d1d2223c21b29d1258b1f211e7886bb859b9a 100644 --- a/testcases/repair/List/List2.scala +++ b/testcases/repair/List/List2.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List3.scala b/testcases/repair/List/List3.scala index 87a1214c77a37845788987bcc931e364bcffdb63..1ad7ef0fd71e8aa8f0d43b31d13e94d261fb45c5 100644 --- a/testcases/repair/List/List3.scala +++ b/testcases/repair/List/List3.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala index 6bee40d1580a6851bbd8a43bc1d8c4da79356a51..0b641cd8079f35a1430f0dd5b96a454f84a7f6d7 100644 --- a/testcases/repair/List/List4.scala +++ b/testcases/repair/List/List4.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala index 46e6e4d50b198ac1251cd4b7a9a208555492eabf..34ae1877d1eb502d426ea5046c2ad12fbecb4dc4 100644 --- a/testcases/repair/List/List5.scala +++ b/testcases/repair/List/List5.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List6.scala b/testcases/repair/List/List6.scala index 028f9410950b6b177eade87fcf617bb70c0d788c..2e1297cb4b6f9f0655c1083de043d0efa2bc1e5b 100644 --- a/testcases/repair/List/List6.scala +++ b/testcases/repair/List/List6.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala index 3faa418ba010075b9650b0a863ee203453f203a1..069dd35d2e65b4387c07095f4c02a00e3741c4f0 100644 --- a/testcases/repair/List/List7.scala +++ b/testcases/repair/List/List7.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala index f7c431cfee66b772b8b8a7e7b3ec595fea80449c..bf99c2e7532aef4b3864a6743ac33401d4b9839c 100644 --- a/testcases/repair/List/List8.scala +++ b/testcases/repair/List/List8.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala index 6969f2f914a7cec2c0ab09152fccd1ec6b8a01b9..59d05b6c526e985341906128506e9b83d50e6ced 100644 --- a/testcases/repair/List/List9.scala +++ b/testcases/repair/List/List9.scala @@ -4,6 +4,7 @@ package leon.custom import leon._ import leon.lang._ +import leon.collection._ import leon.annotation._ sealed abstract class List0[T] { diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala index f8515bade6e7084d3af05874b91893c6cb89f90f..901d4c6a270f49a7902d2cc9e41eb27c93a96184 100644 --- a/testcases/repair/MergeSort/MergeSort1.scala +++ b/testcases/repair/MergeSort/MergeSort1.scala @@ -1,3 +1,5 @@ +import leon.lang._ + object MergeSort { abstract class List { diff --git a/testcases/repair/RedBlackTree/RedBlackTree.scala b/testcases/repair/RedBlackTree/RedBlackTree.scala index d80fafc0856ac5edca73569101e7bc0fd06a1e28..8bf916e87dbaff0754d90843b8ee12b01103fbcd 100644 --- a/testcases/repair/RedBlackTree/RedBlackTree.scala +++ b/testcases/repair/RedBlackTree/RedBlackTree.scala @@ -1,5 +1,5 @@ -import leon._ -import lang._ +import leon.lang._ +import leon.collection._ import annotation._ object RedBlackTree { diff --git a/testcases/repair/RedBlackTree/RedBlackTree1.scala b/testcases/repair/RedBlackTree/RedBlackTree1.scala index d219c00949a6606cb0c6a237b76053fd9fc3c799..c19819441f00de6ae86f666aac2c312c650da851 100644 --- a/testcases/repair/RedBlackTree/RedBlackTree1.scala +++ b/testcases/repair/RedBlackTree/RedBlackTree1.scala @@ -1,5 +1,5 @@ -import leon._ -import lang._ +import leon.lang._ +import leon.collection._ import annotation._ object RedBlackTree { diff --git a/testcases/repair/RedBlackTree/RedBlackTree2.scala b/testcases/repair/RedBlackTree/RedBlackTree2.scala index 7f0c029c8d514f3d722f095429eb6fb117bd5b79..a02dcb6f4224c9d27c23f55b2f238671a8e7801a 100644 --- a/testcases/repair/RedBlackTree/RedBlackTree2.scala +++ b/testcases/repair/RedBlackTree/RedBlackTree2.scala @@ -1,5 +1,5 @@ -import leon._ -import lang._ +import leon.lang._ +import leon.collection._ import annotation._ object RedBlackTree { diff --git a/testcases/repair/RedBlackTree/RedBlackTree3.scala b/testcases/repair/RedBlackTree/RedBlackTree3.scala index a5d561985646e766f7ab6f19136075fbc69dad8e..ffacf352ebfd2adf85e1aaebdbe8026600034dd6 100644 --- a/testcases/repair/RedBlackTree/RedBlackTree3.scala +++ b/testcases/repair/RedBlackTree/RedBlackTree3.scala @@ -1,5 +1,5 @@ -import leon._ -import lang._ +import leon.lang._ +import leon.collection._ import annotation._ object RedBlackTree { diff --git a/testcases/repair/RedBlackTree/RedBlackTree6.scala b/testcases/repair/RedBlackTree/RedBlackTree6.scala index 9eed1ac3a1efbf46cd9fbd95c71aba4d898a15aa..82e0372d5ef33a50adc7ac44652a9da1c37454f6 100644 --- a/testcases/repair/RedBlackTree/RedBlackTree6.scala +++ b/testcases/repair/RedBlackTree/RedBlackTree6.scala @@ -1,5 +1,5 @@ -import leon._ -import lang._ +import leon.lang._ +import leon.collection._ import annotation._ object RedBlackTree { diff --git a/testcases/repair/inria/FirstIndexOf.scala b/testcases/repair/inria/FirstIndexOf.scala index d591315063d90c26b2adfbe7bdd36b03d4871a99..2693d18cd62cdcb52ef924343f47d2c349633ca8 100644 --- a/testcases/repair/inria/FirstIndexOf.scala +++ b/testcases/repair/inria/FirstIndexOf.scala @@ -4,7 +4,7 @@ import leon.lang.synthesis._ object FirstIndexOf { - def firstIndexOf(l: List[Int], v: Int): Int = { + def firstIndexOf(l: List[Int], v: Int): BigInt = { l match { case Cons(h, t) if v == h => 0 case Cons(h, t) => @@ -17,7 +17,7 @@ object FirstIndexOf { -1 } } ensuring { - (res: Int) => (if (l.content contains v) { + (res: BigInt) => (if (l.content contains v) { l.size > res && l.apply(res) == v } else { res == -1 diff --git a/testcases/repair/inria/HeapSort.scala b/testcases/repair/inria/HeapSort.scala index 5ceed2228715ceb2ea9bb7270c81c3608698a6a9..46be0f31a1a0855d31ed4b0ec929aa3d7cb5a49a 100644 --- a/testcases/repair/inria/HeapSort.scala +++ b/testcases/repair/inria/HeapSort.scala @@ -4,8 +4,8 @@ * Date: 20.11.2013 **/ +import leon.lang._ import leon.collection._ -import leon._ object HeapSort { diff --git a/testcases/synthesis/NewYearsSong.scala b/testcases/synthesis/NewYearsSong.scala deleted file mode 100644 index 0bcdf0130dd4dfc76b664a28e2bd19cadac75f0a..0000000000000000000000000000000000000000 --- a/testcases/synthesis/NewYearsSong.scala +++ /dev/null @@ -1,28 +0,0 @@ -import leon.lang.synthesis._ -import leon.annotation._ -import leon.lang._ - -object NewYearSong { - - def computeLines(eLines: Int, - iLines: Int, - iSyls: Int, - nSyls: Int) : (Int,Int,Int,Int,Int,Int) = { - choose((line7: Int, - line8: Int, - nsLines: Int, - nLines: Int, - tLines: Int, - tLinesFact: Int) => ( - tLines == eLines + nLines - && nLines == iLines + nsLines - && nLines == line7 + line8 - && nSyls + iSyls == 7 * line7 + 8 * line8 - && tLines == 4 * tLinesFact // expresses (4 | tLines) - && line8 >= 0 - && line7 >= 0 - && tLines >= 0 - )) - } - -} diff --git a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala index b966885e6e3505a78bd5501a1cf96f30a8a38b88..64a8ae73ddd8553ff4ca364814aa880c41b503f8 100644 --- a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala +++ b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueue.scala @@ -1,4 +1,5 @@ -import scala.collection.immutable.Set +import leon.lang._ +import leon.collection._ import leon.lang._ diff --git a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala index 467fc66dfb4a8e99d7043f9b3ffeef519d1712df..c0697de3f62793ef7da4dfbe72ccaa8ad10d6bc4 100644 --- a/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala +++ b/testcases/synthesis/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala @@ -1,6 +1,5 @@ -import scala.collection.immutable.Set - import leon.lang._ +import leon.collection._ object BatchedQueue { sealed abstract class List diff --git a/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala index 2e3f168a37939fb67a1203c35a8cc0b4ea3fd4c7..bcc6d17ab28c023a63e1ea508d34bdd8ee2e2975 100644 --- a/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala +++ b/testcases/synthesis/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala b/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala deleted file mode 100644 index 240a5f0091356f4bcdb8c78c972c566f71e60c7c..0000000000000000000000000000000000000000 --- a/testcases/synthesis/condabd/benchmarks/List/ListSearch.scala +++ /dev/null @@ -1,50 +0,0 @@ -import leon.lang._ - -object ListOperations { - sealed abstract class List - case class Cons(head: Int, tail: List) extends List - case class Nil() extends List - - sealed abstract class Option - case class Some(i: Int) extends Option - case object None extends Option - - def content(l: List) : Set[Int] = l match { - case Nil() => Set.empty - case Cons(head, tail) => Set(head) ++ content(tail) - } - - def size(l: List) : Int = l match { - case Nil() => 0 - case Cons(head, tail) => 1 + size(tail) - } -// -// def isEmpty(l: List) = l match { -// case Nil() => true -// case Cons(_, _) => false -// } - - - def linearSearch(l: List, c: Int): Option = { - l match { - case Nil() => None - case Cons(lHead, lTail) => - if (lHead == c) Some(size(l)) - else Some(linearSearch(lTail, c)) - } - } ensuring(res => if(res > -1) atInd(l, size(l) - res) == c else !content(l).contains(c)) - - def atInd(l: List, ind: Int): Int = { - require(ind >= 0 && ind < size(l)) - - l match { - case Nil() => -1 - case Cons(lHead, lTail) => - if (ind == 0) lHead - else atInd(lTail, ind - 1) - } - - } ensuring( res => - if (size(l) == 0) res == -1 else content(l).contains(res) - ) -} diff --git a/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala index 1fadb1d803d96cd78377f2dbb52f355b3fcd2365..ad20d41b24816b2237e87f35961c833ca492926f 100644 --- a/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala +++ b/testcases/synthesis/condabd/benchmarks/MergeSort/MergeSortMerge.scala @@ -30,7 +30,7 @@ object MergeSort { def merge(aList : List, bList : List) : List = { require(isSorted(aList) && isSorted(bList)) choose( (res: List) => - ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res)) + contents(res) == contents(aList) ++ contents(bList) && isSorted(res) ) } diff --git a/testcases/synthesis/insynth-leon-tests/Arguments.scala b/testcases/synthesis/insynth-leon-tests/Arguments.scala deleted file mode 100644 index 75b4eceaaf629f5ed479faebbf6f38bfcd146f07..0000000000000000000000000000000000000000 --- a/testcases/synthesis/insynth-leon-tests/Arguments.scala +++ /dev/null @@ -1,13 +0,0 @@ -import leon.annotation._ -import leon.lang._ - -object Hole { - - def method(t: Int, x: Boolean, y: Boolean) : Int = ({ - if (t > 5) - hole(5) - else - t - }) ensuring ( _ > 0 ) - -} diff --git a/testcases/synthesis/io-examples/List.scala b/testcases/synthesis/io-examples/List.scala index 01214c727aefb3266aba6e62ca1dcb09c2df55bb..0e2d2b0fddb909e6a06ac666b6371d7e518991d9 100644 --- a/testcases/synthesis/io-examples/List.scala +++ b/testcases/synthesis/io-examples/List.scala @@ -9,11 +9,11 @@ object Foo { //Cons[Int](i, l).slice(0, i) ???[List[Int]] } ensuring { (res: List[Int]) => - passes((l, i), res)(Map[(List[Int], Int), List[Int]]( - (Nil[Int](), 2) -> Cons(2, Nil[Int]()), - (Cons(1, Nil()), 2) -> Cons(2, Cons(1, Nil())), - (Cons(1, Cons(2, Cons(3, Nil()))), 3) -> Cons(3, Cons(1, Cons(2, Nil()))) - )) + ((l, i), res) passes { + case (Nil(), 2) => Cons(2, Nil[Int]()) + case (Cons(1, Nil()), 2) => Cons(2, Cons(1, Nil())) + case (Cons(1, Cons(2, Cons(3, Nil()))), 3) => Cons(3, Cons(1, Cons(2, Nil()))) + } } } diff --git a/testcases/synthesis/io-examples/Lists.scala b/testcases/synthesis/io-examples/Lists.scala index 62335cc362ded88ec3118a8456e91a2a102d6d8f..7d3d068e0bfb279feee9fdfcbc0674eba84bd5a4 100644 --- a/testcases/synthesis/io-examples/Lists.scala +++ b/testcases/synthesis/io-examples/Lists.scala @@ -5,18 +5,18 @@ import leon.lang.synthesis._ object Lists { def safetail(l: List[Int]): List[Int] = choose { (res : List[Int]) => - passes(l, res)(Map( - Cons(1, Cons(2, Cons(3, Cons(4, Nil())))) -> Cons(2, Cons(3, Cons(4, Nil()))), - Cons(2, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())), - Nil() -> Nil() - )) + (l, res) passes { + case Cons(1, Cons(2, Cons(3, Cons(4, Nil())))) => Cons(2, Cons(3, Cons(4, Nil()))) + case Cons(2, Cons(3, Cons(4, Nil()))) => Cons(3, Cons(4, Nil())) + case Nil() => Nil() + } } def uniq(l: List[Int]): List[Int] = choose { (res : List[Int]) => - passes(l, res)(Map( - Cons(1, Cons(1, Cons(1, Cons(2, Nil())))) -> Cons(1, Cons(2, Nil())), - Cons(3, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())), - Nil() -> Nil() - )) + (l, res) passes { + case Cons(1, Cons(1, Cons(1, Cons(2, Nil())))) => Cons(1, Cons(2, Nil())) + case Cons(3, Cons(3, Cons(4, Nil()))) => Cons(3, Cons(4, Nil())) + case Nil() => Nil() + } } } diff --git a/testcases/synthesis/io-examples/Math.scala b/testcases/synthesis/io-examples/Math.scala index df68735e3c46fe0c154a56023c3b86d774d1d40d..2e50289d6ba4cc31c695eaac16ad1863410e3dcf 100644 --- a/testcases/synthesis/io-examples/Math.scala +++ b/testcases/synthesis/io-examples/Math.scala @@ -10,25 +10,17 @@ object Math { } else { ???[Int] } - } ensuring { - passes(a, _)(Map( - 0 -> 0, - 1 -> 1, - 2 -> 1, - 3 -> 2, - 4 -> 3, - 5 -> 5, - 18 -> 2584 - )) - } - - def abs(a: Int): Int = { - if (?(a >= 0, a <= 0, a == 0, a != 0)) { - a - } else { - -a + } ensuring { res => + (a, res) passes { + case 0 => 0 + case 1 => 1 + case 2 => 1 + case 3 => 2 + case 4 => 3 + case 5 => 5 + case 18 => 2584 } - } ensuring { _ >= 0 } + } diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala deleted file mode 100644 index 7dbb6bfc37072d53ffb99f65b02a8b79693c4d55..0000000000000000000000000000000000000000 --- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala +++ /dev/null @@ -1,91 +0,0 @@ -import scala.collection.immutable.Set - -import leon.lang._ - -object BatchedQueue { - sealed abstract class List - case class Cons(head: Int, tail: List) extends List - case object Nil extends List - - def content(l: List): Set[Int] = l match { - case Nil => Set.empty - case Cons(head, tail) => Set(head) ++ content(tail) - } - - def content(p: Queue): Set[Int] = - content(p.f) ++ content(p.r) - - case class Queue(f: List, r: List) - - def rev_append(aList: List, bList: List): List = (aList match { - case Nil => bList - case Cons(x, xs) => rev_append(xs, Cons(x, bList)) - }) ensuring ( - res => - content(res) == content(aList) ++ content(bList) && - size(res) == size(aList) + size(bList) - ) - - def invariantList(q:Queue, f: List, r: List): Boolean = ({ - rev_append(q.f, q.r) == rev_append(f, r) - }) ensuring ( - res => - true - ) - - def reverse(list: List) = rev_append(list, Nil) ensuring ( - res => - content(res) == content(list) && size(res) == size(list) - ) - - def checkf(f: List, r: List): Queue = (f match { - case Nil => Queue(reverse(r), Nil) - case _ => Queue(f, r) - }) ensuring { - res => content(res) == content(f) ++ content(r) && - size(res) == size(f) + size(r) && - invariantList(res, f, r) - } - - def head(p: Queue): Set[Int] = ( - p.f match { - case Nil => Set[Int]() - case Cons(x, xs) => Set(x) - }) ensuring ( - res => - if (isEmpty(p)) true - else content(p) == res ++ content(tail(p))) - - def tail(p: Queue): Queue = { - require(!isEmpty(p)) - p.f match { - case Nil => p - case Cons(_, xs) => checkf(xs, p.r) - } - } ensuring { - (res: Queue) => content(res) ++ head(p) == content(p) && - (if (isEmpty(p)) true - else size(res) + 1 == size(p)) - } - // - // def last(p: Queue): Int = { - // require(!isEmpty(p)) - // p.r match { - // case Nil => reverse(p.f).asInstanceOf[Cons].head - // case Cons(x, _) => x - // } - // } - - def snoc(p: Queue, x: Int): Queue = - checkf(p.f, Cons(x, p.r)) ensuring ( - res => - content(res) == content(p) ++ Set(x) && - size(res) == size(p) + 1 && - ( - if (isEmpty(p)) true - else (content(tail(res)) ++ Set(x) == content(tail(res)) && - size(res.f) == size(p.f)) - ) - ) - -} diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala deleted file mode 100644 index 310b7e7e28afd45e65d5056dc784b87b36cd5744..0000000000000000000000000000000000000000 --- a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala +++ /dev/null @@ -1,48 +0,0 @@ -import scala.collection.immutable.Set -import leon.annotation._ -import leon.lang._ - -object InsertionSort { - sealed abstract class List - case class Cons(head: Int, tail: List) extends List - case class Nil() extends List - - def size(l: List): Int = (l match { - case Nil() => 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 insert(e: Int, l: List): List = { - 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) - && isSorted(res) - && size(res) == size(l) + 1) - - /* Insertion sort yields a sorted list of same size and content as the input - * list */ - def sort(l: List): List = (l match { - case Nil() => Nil() - case Cons(x, xs) => sortedIns(x, sort(xs)) - }) ensuring (res => contents(res) == contents(l) - && isSorted(res) - && size(res) == size(l)) - -} diff --git a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala index 062578c96d34459500eca24eeed3e008a3e9a12b..326295aafafdb88a71d0cd2c25f740efe0438fc9 100644 --- a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala +++ b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable.Set - import leon.lang._ object MergeSort { diff --git a/testcases/synthesis/oopsla2013/SortedList/Batch.scala b/testcases/synthesis/oopsla2013/SortedList/Batch.scala index 35e60c8d887185c4ffd8c896918ad74250670719..8da614143ef31571bbe112a53af48fb2bd89bd12 100644 --- a/testcases/synthesis/oopsla2013/SortedList/Batch.scala +++ b/testcases/synthesis/oopsla2013/SortedList/Batch.scala @@ -47,7 +47,7 @@ object SortedList { choose { (out : List) => - && (content(out) == content(in1) ++ content(in2)) && isSorted(out) + (content(out) == content(in1) ++ content(in2)) && isSorted(out) } } @@ -56,7 +56,7 @@ object SortedList { choose { (out : List) => - && (content(out) == content(in1) -- content(in2)) && isSorted(out) + (content(out) == content(in1) -- content(in2)) && isSorted(out) } } diff --git a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala index 2cf542ae5fc761e088836d37610ffb26b5dba061..8683e0b5a291fde438d4da03f7f72c390ab8d753 100644 --- a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala +++ b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala @@ -107,7 +107,7 @@ object SparseVector { case Nil => None } - } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)) } + } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res))) } // def get(sv: SparseVector, at: Int): Option = choose { // (res: Option) => invariant(sv) && ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res))) diff --git a/testcases/verification/Addresses.scala b/testcases/verification/Addresses.scala index cd089c44cfce8f966e6f6ff98d3511c9dae796d2..bc6ad57b8fa7e0a6c215aa216e2ae9b9322ec9b6 100644 --- a/testcases/verification/Addresses.scala +++ b/testcases/verification/Addresses.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/datastructures/BinarySearchTree.scala b/testcases/verification/datastructures/BinarySearchTree.scala index 471813c13191d6437fc9c4995ec560308e62b88a..ef87a00eab9b59870278a2291db888cfd82d9abc 100644 --- a/testcases/verification/datastructures/BinarySearchTree.scala +++ b/testcases/verification/datastructures/BinarySearchTree.scala @@ -1,3 +1,6 @@ +import leon.lang._ +import leon.collection._ + object BSTSimpler { sealed abstract class Tree case class Node(left: Tree, value: Int, right: Tree) extends Tree diff --git a/testcases/verification/datastructures/BinarySearchTreeSorted.scala b/testcases/verification/datastructures/BinarySearchTreeSorted.scala index 464335f62c09ee9934b801108d0c8494b52ee54d..577e0e6a02a90260e484b33d2ce1f3f54a08c93d 100644 --- a/testcases/verification/datastructures/BinarySearchTreeSorted.scala +++ b/testcases/verification/datastructures/BinarySearchTreeSorted.scala @@ -1,6 +1,6 @@ import leon.lang._ import leon.annotation._ -import leon._ +import leon.collection._ object BinaryTree { sealed abstract class Tree diff --git a/testcases/verification/datastructures/InsertionSort.scala b/testcases/verification/datastructures/InsertionSort.scala index 1781531cb79175716fa7e8e098594d5c99d35f0a..fcb2b94d59464dfc815e23fba7aae6b10aea2d99 100644 --- a/testcases/verification/datastructures/InsertionSort.scala +++ b/testcases/verification/datastructures/InsertionSort.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ object InsertionSort { diff --git a/testcases/verification/datastructures/ListWithSize.scala b/testcases/verification/datastructures/ListWithSize.scala index 660f09a433d571b31daddda5a8124cf0c75bf331..d826eae580e62dcd69a1b4f0a4c1806f92cd7b6b 100644 --- a/testcases/verification/datastructures/ListWithSize.scala +++ b/testcases/verification/datastructures/ListWithSize.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/datastructures/MergeSort.scala b/testcases/verification/datastructures/MergeSort.scala index 408830ced0fd44c09f50238edfaa9d0012ffb234..1bbd7f607528a9549363dec4d3e73f547f602565 100644 --- a/testcases/verification/datastructures/MergeSort.scala +++ b/testcases/verification/datastructures/MergeSort.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object MergeSort { sealed abstract class List diff --git a/testcases/verification/datastructures/QuickSort.scala b/testcases/verification/datastructures/QuickSort.scala index a5f03f21492d56013edc77a49b30ca1e33cbb121..cb193d2c89b012d851e9f106b1d33518aaf1b0fc 100644 --- a/testcases/verification/datastructures/QuickSort.scala +++ b/testcases/verification/datastructures/QuickSort.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object QuickSort { sealed abstract class List diff --git a/testcases/verification/datastructures/RedBlackTree.scala b/testcases/verification/datastructures/RedBlackTree.scala index 98a70c1911d97ab2518dec9b73a445d6ca9ff15d..eb998becb34319e1ccfdb7230c9d314617a7854f 100644 --- a/testcases/verification/datastructures/RedBlackTree.scala +++ b/testcases/verification/datastructures/RedBlackTree.scala @@ -1,5 +1,4 @@ -import scala.collection.immutable.Set -//import scala.collection.immutable.Multiset +import leon.lang._ object RedBlackTree { sealed abstract class Color diff --git a/testcases/verification/datastructures/SortedList.scala b/testcases/verification/datastructures/SortedList.scala index 41451641beaa7917e3fbfa9621d0cdbb53f05893..91b3e2af3998d53221ba89f90226643fc57dcae7 100644 --- a/testcases/verification/datastructures/SortedList.scala +++ b/testcases/verification/datastructures/SortedList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/datastructures/TreeListSetNoDup.scala b/testcases/verification/datastructures/TreeListSetNoDup.scala index 44d7fcf0b10d4a4a6c5dd5dd702ff2c4ccb967f8..ef72d3a6839548d541df8cece6dd4c00169bf56d 100644 --- a/testcases/verification/datastructures/TreeListSetNoDup.scala +++ b/testcases/verification/datastructures/TreeListSetNoDup.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/MST/MSTMap.scala b/testcases/verification/graph/MST/MSTMap.scala index da2a08fc0052f4cb96c23b72e7a5fcb217dae26b..1ef72da321d96c6b65977427c2aff485212c990e 100644 --- a/testcases/verification/graph/MST/MSTMap.scala +++ b/testcases/verification/graph/MST/MSTMap.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/SortedNDList.scala b/testcases/verification/graph/SortedNDList.scala index 98c06e7c95ac7c6f68a7b61f9a35b54bc85661e4..42a16cfbd8cdea49a1c5c8a17e61d8dab052dc67 100644 --- a/testcases/verification/graph/SortedNDList.scala +++ b/testcases/verification/graph/SortedNDList.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/Subgraph.scala b/testcases/verification/graph/Subgraph.scala index 2f60f78f07cb4f417a6f94381a101b9621d9af13..5e17811376e4b4f17a56dc53d22c5ca5fe7ca3ac 100644 --- a/testcases/verification/graph/Subgraph.scala +++ b/testcases/verification/graph/Subgraph.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/SubgraphMap.scala b/testcases/verification/graph/SubgraphMap.scala index 90522ba9c64eb052180ec288940e0d52b39d5662..3714d2eb7a2ab1ded4f2a01ed5aa72ef6c3f196c 100644 --- a/testcases/verification/graph/SubgraphMap.scala +++ b/testcases/verification/graph/SubgraphMap.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/TreeEquivalence.scala b/testcases/verification/graph/TreeEquivalence.scala index c059473ea82a6643212ccdb9d71712156d18c8e4..a12c82ed337ef91ef839af1114fe0b81d15ace16 100644 --- a/testcases/verification/graph/TreeEquivalence.scala +++ b/testcases/verification/graph/TreeEquivalence.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/TreeEquivalenceMap.scala b/testcases/verification/graph/TreeEquivalenceMap.scala index e0dd4bca5d16ecafcfa8ee847ca4df0faae719a6..7c4a1103c0f3ef5a0974d2b034259ea4c39361fc 100644 --- a/testcases/verification/graph/TreeEquivalenceMap.scala +++ b/testcases/verification/graph/TreeEquivalenceMap.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala index d3958a893cf86a5550db490c83f06bc387014f4b..20461a2566544e3c61e7d3c5a59f1483651f6d3e 100644 --- a/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala +++ b/testcases/verification/graph/dijkstras/DijkstrasSortedList.scala @@ -1,5 +1,3 @@ -import scala.collection.immutable._ - import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/higher-order/invalid/Continuations1.scala b/testcases/verification/higher-order/invalid/Continuations1.scala index 82f4bdea42f7b121205a1b09a113b732d58020fb..0d65fc817fc2680b0127c89eb7bbd40da80ba384 100644 --- a/testcases/verification/higher-order/invalid/Continuations1.scala +++ b/testcases/verification/higher-order/invalid/Continuations1.scala @@ -1,4 +1,5 @@ import leon.lang._ +import leon.collection._ object Continuations1 { def add_cps[T](x: BigInt, y: BigInt)(f: BigInt => T): T = { diff --git a/testcases/verification/higher-order/invalid/HOInvocations.scala b/testcases/verification/higher-order/invalid/HOInvocations.scala index 3d2e16835a7347ed4140e9902ec330ae3d058ea9..bf1f40a4373e6869d2813904b2798ef3224e16c6 100644 --- a/testcases/verification/higher-order/invalid/HOInvocations.scala +++ b/testcases/verification/higher-order/invalid/HOInvocations.scala @@ -1,4 +1,5 @@ import leon.lang._ +import leon.collection._ object HOInvocations { def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g diff --git a/testcases/verification/higher-order/invalid/Lists1.scala b/testcases/verification/higher-order/invalid/Lists1.scala index e7582fad659cd8bb50d8cfc3eed63dc2740013a4..7fc938a51918461f68e6e4ef1ec611c216731802 100644 --- a/testcases/verification/higher-order/invalid/Lists1.scala +++ b/testcases/verification/higher-order/invalid/Lists1.scala @@ -1,4 +1,5 @@ import leon.lang._ +import leon.collection._ object Lists1 { abstract class List[T] diff --git a/testcases/verification/higher-order/invalid/Lists2.scala b/testcases/verification/higher-order/invalid/Lists2.scala index 777223617e03f2e1f95a4eaf3d08b734de03599d..59faa779becb2c58ec638a4d26621a8b24dca9c4 100644 --- a/testcases/verification/higher-order/invalid/Lists2.scala +++ b/testcases/verification/higher-order/invalid/Lists2.scala @@ -1,6 +1,4 @@ -import leon._ import leon.lang._ -import leon.annotation._ import leon.collection._ diff --git a/testcases/verification/higher-order/invalid/ParBalance.scala b/testcases/verification/higher-order/invalid/ParBalance.scala index 4a2a93c23fe49bc191a158c0b205f606166cd85e..62eca559db1e139d719e5b4215b0867ea91e9c35 100644 --- a/testcases/verification/higher-order/invalid/ParBalance.scala +++ b/testcases/verification/higher-order/invalid/ParBalance.scala @@ -1,5 +1,5 @@ -import leon._ import leon.lang._ +import leon.collection._ object ParBalance { diff --git a/testcases/verification/higher-order/invalid/PositiveMap.scala b/testcases/verification/higher-order/invalid/PositiveMap.scala index fb1452f478b7e71f3d9d23093553a05aa0d3af1b..7fb002360005248db3f752eec9d77214b7e0a316 100644 --- a/testcases/verification/higher-order/invalid/PositiveMap.scala +++ b/testcases/verification/higher-order/invalid/PositiveMap.scala @@ -1,4 +1,5 @@ import leon.lang._ +import leon.collection._ object PositiveMap { diff --git a/testcases/verification/higher-order/invalid/Sets1.scala b/testcases/verification/higher-order/invalid/Sets1.scala index 45545c356882ca5cb37966a05e23fe6211030f94..62d1409b0eea5f895f35808a57ec21d7600edf5d 100644 --- a/testcases/verification/higher-order/invalid/Sets1.scala +++ b/testcases/verification/higher-order/invalid/Sets1.scala @@ -1,4 +1,5 @@ import leon.lang._ +import leon.collection._ object Sets1 { def set(i: Int): Int => Boolean = x => x == i diff --git a/testcases/verification/higher-order/invalid/Transformation.scala b/testcases/verification/higher-order/invalid/Transformation.scala index 83c265aee58649a30d9214626905db41d626b38d..9c9bf86bcb2e2965522bb81463d7b124d7fadea3 100644 --- a/testcases/verification/higher-order/invalid/Transformation.scala +++ b/testcases/verification/higher-order/invalid/Transformation.scala @@ -1,5 +1,5 @@ -import leon._ import leon.lang._ +import leon.collection._ object Transformation { diff --git a/testcases/verification/pldi2011-testcases/AssociativeList.scala b/testcases/verification/pldi2011-testcases/AssociativeList.scala index 2b99141b2f57708ad03565f8380589adc84c2863..5f5dd8ae1c870bb04b4c5ba1688a776fff4ed585 100644 --- a/testcases/verification/pldi2011-testcases/AssociativeList.scala +++ b/testcases/verification/pldi2011-testcases/AssociativeList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/pldi2011-testcases/ForElimination.scala b/testcases/verification/pldi2011-testcases/ForElimination.scala index fe96501331a6f39ca9c794d75341d98b6fb58eeb..0e478762b2385434f502c75c2e9e36e155d01abe 100644 --- a/testcases/verification/pldi2011-testcases/ForElimination.scala +++ b/testcases/verification/pldi2011-testcases/ForElimination.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/pldi2011-testcases/InsertionSort.scala b/testcases/verification/pldi2011-testcases/InsertionSort.scala index 3e606fe8b41d96c284ebf261ab58af1ee6016172..a201e6eb1ff216b16c5c925bafb9cdc156d416f0 100644 --- a/testcases/verification/pldi2011-testcases/InsertionSort.scala +++ b/testcases/verification/pldi2011-testcases/InsertionSort.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/pldi2011-testcases/LambdaEval.scala b/testcases/verification/pldi2011-testcases/LambdaEval.scala index 4dde6b2bc88bca4e0fd5295903c7a33b83474d95..84ecf4737b43fbca5ea229495e71d7e048089f88 100644 --- a/testcases/verification/pldi2011-testcases/LambdaEval.scala +++ b/testcases/verification/pldi2011-testcases/LambdaEval.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/pldi2011-testcases/ListTree.scala b/testcases/verification/pldi2011-testcases/ListTree.scala index 5057b155b406e9880eca8016ecf0560e3f16c487..edcd48650cb6a3da48d61d18c1e27829803e04a8 100644 --- a/testcases/verification/pldi2011-testcases/ListTree.scala +++ b/testcases/verification/pldi2011-testcases/ListTree.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object ListTree { /* Trees holding integers and internal lists */ diff --git a/testcases/verification/pldi2011-testcases/MergeSort.scala b/testcases/verification/pldi2011-testcases/MergeSort.scala index 4e0121ac4e95df4d37ba52bb4a57d8b4f42986ad..96e81e40e086b559118efed8d619353c77637ab3 100644 --- a/testcases/verification/pldi2011-testcases/MergeSort.scala +++ b/testcases/verification/pldi2011-testcases/MergeSort.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ object MergeSort { sealed abstract class List diff --git a/testcases/verification/pldi2011-testcases/PropositionalLogic.scala b/testcases/verification/pldi2011-testcases/PropositionalLogic.scala index 0270bdf87ae8cea34d98afcbfe6f1ca164d7ed57..8356d2cbf3ba173d5d4f1b140a82019e10c98c76 100644 --- a/testcases/verification/pldi2011-testcases/PropositionalLogic.scala +++ b/testcases/verification/pldi2011-testcases/PropositionalLogic.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/pldi2011-testcases/QuickSort.scala b/testcases/verification/pldi2011-testcases/QuickSort.scala index a0a151057edd315422d87236b793b1672a64a9ac..30b3621438bd0ef944b61f831b36379deb1470f6 100644 --- a/testcases/verification/pldi2011-testcases/QuickSort.scala +++ b/testcases/verification/pldi2011-testcases/QuickSort.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/pldi2011-testcases/RedBlackTree.scala b/testcases/verification/pldi2011-testcases/RedBlackTree.scala index 3ebfa25e2a4fbfbeaf1fd470848276747c19c87d..c7f380df8a91c0184c6dc8f6eac7a577cf821a85 100644 --- a/testcases/verification/pldi2011-testcases/RedBlackTree.scala +++ b/testcases/verification/pldi2011-testcases/RedBlackTree.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala b/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala index 585135d06645f4e4fc250d878b3808a797f3f5f9..fed0247b6b4c746e6f576b997d9ba03ce2b3e940 100644 --- a/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala +++ b/testcases/verification/pldi2011-testcases/RedBlackTreeDeletion.scala @@ -1,4 +1,4 @@ -import scala.collection.immutable.Set +import leon.lang._ import leon.annotation._ object RedBlackTree { @@ -238,7 +238,7 @@ object RedBlackTree { val maxV = max(l) val newL = removeMax(l) bubble(c, newL, maxV, r) - case _ => throw new Exception("Removing an unexpected tree") + case _ => error[Tree]("Removing an unexpected tree") } } ensuring(res => hasRedBlackDesc(res)) diff --git a/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala b/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala index 034ec122247d26a805518a44ce13c9a0538cb7a9..0a10b118d235fb5f7d33f5309c782ea443415615 100644 --- a/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala +++ b/testcases/verification/pldi2011-testcases/SemanticsPreservation.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/pldi2011-testcases/TreeMap.scala b/testcases/verification/pldi2011-testcases/TreeMap.scala index 44b85cff7e4b0df9586939bcefd43cd5398ef66c..ce6fd7f8170eb2115d245390b4b82f55a5aa5535 100644 --- a/testcases/verification/pldi2011-testcases/TreeMap.scala +++ b/testcases/verification/pldi2011-testcases/TreeMap.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ object TreeMap { diff --git a/testcases/verification/sas2011-testcases/AmortizedQueue.scala b/testcases/verification/sas2011-testcases/AmortizedQueue.scala index a3636e00aa2141d95c814a7448d6be950710c906..d5caf37ec30ab6ce0f7d26f56da07e0a9b9dd441 100644 --- a/testcases/verification/sas2011-testcases/AmortizedQueue.scala +++ b/testcases/verification/sas2011-testcases/AmortizedQueue.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/sas2011-testcases/AssociativeList.scala b/testcases/verification/sas2011-testcases/AssociativeList.scala index 6567c4786e3ef021d5e1f8a4c2de91562418766e..3b4e954a87a07a7bfb128427d20454d36d4435eb 100644 --- a/testcases/verification/sas2011-testcases/AssociativeList.scala +++ b/testcases/verification/sas2011-testcases/AssociativeList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/sas2011-testcases/InsertionSort.scala b/testcases/verification/sas2011-testcases/InsertionSort.scala index b01d0ae2f292b8a27a9ec911d167a50478a93ce3..5c7419ce54aa4c9871275bbdc37b4163f89c6f34 100644 --- a/testcases/verification/sas2011-testcases/InsertionSort.scala +++ b/testcases/verification/sas2011-testcases/InsertionSort.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/sas2011-testcases/ListOperations.scala b/testcases/verification/sas2011-testcases/ListOperations.scala index 2cba911ada05b76afc8bd7cf906c0ed196e9a7fd..991febc577600d9e3d960745e8cd1ab64488dd89 100644 --- a/testcases/verification/sas2011-testcases/ListOperations.scala +++ b/testcases/verification/sas2011-testcases/ListOperations.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/sas2011-testcases/PropositionalLogic.scala b/testcases/verification/sas2011-testcases/PropositionalLogic.scala index ca410a5ae541201b399dd680fc05a9427e9394ee..efc8f8f87b468b9b7a1283e3476a901e1cb32a2a 100644 --- a/testcases/verification/sas2011-testcases/PropositionalLogic.scala +++ b/testcases/verification/sas2011-testcases/PropositionalLogic.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/sas2011-testcases/RedBlackTree.scala b/testcases/verification/sas2011-testcases/RedBlackTree.scala index e77838fff0d92429c7cea9065ec69c775e3151de..0e6603209f079d23a95560bdb576e7ef719a426c 100644 --- a/testcases/verification/sas2011-testcases/RedBlackTree.scala +++ b/testcases/verification/sas2011-testcases/RedBlackTree.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/sas2011-testcases/SearchLinkedList.scala b/testcases/verification/sas2011-testcases/SearchLinkedList.scala index 40f29050f030f2ab260580d5d03df9db42de2477..14e36d3e4e829b6ed5694a83f17cc80a57d9cdf1 100644 --- a/testcases/verification/sas2011-testcases/SearchLinkedList.scala +++ b/testcases/verification/sas2011-testcases/SearchLinkedList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/scala2013/AmortizedQueue.scala b/testcases/verification/scala2013/AmortizedQueue.scala index 52e4ed7e2c313d83b46f766e7694e152ca4c19b9..467a39d4865c7433c9ecf92704a09e1400ecd71d 100644 --- a/testcases/verification/scala2013/AmortizedQueue.scala +++ b/testcases/verification/scala2013/AmortizedQueue.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/scala2013/AmortizedQueueImp.scala b/testcases/verification/scala2013/AmortizedQueueImp.scala index afaefbca1b6db09abf8e8cc34e7dfd50ec3b7a44..fb3d5497098e7519e9581e735386581116fce39e 100644 --- a/testcases/verification/scala2013/AmortizedQueueImp.scala +++ b/testcases/verification/scala2013/AmortizedQueueImp.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/scala2013/AssociativeList.scala b/testcases/verification/scala2013/AssociativeList.scala index 6567c4786e3ef021d5e1f8a4c2de91562418766e..3b4e954a87a07a7bfb128427d20454d36d4435eb 100644 --- a/testcases/verification/scala2013/AssociativeList.scala +++ b/testcases/verification/scala2013/AssociativeList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/scala2013/AssociativeListImp.scala b/testcases/verification/scala2013/AssociativeListImp.scala index d15101ec7050f106dc7ad60859f4f60e17fac956..3810203c003589a036fb64fd8b949b737d4c2eaa 100644 --- a/testcases/verification/scala2013/AssociativeListImp.scala +++ b/testcases/verification/scala2013/AssociativeListImp.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/scala2013/ListOperations.scala b/testcases/verification/scala2013/ListOperations.scala index 86d0f522f69633e0321da4d52bb32352b7cc1239..157c6b978eb4c2b1f5c2f9e7091f81b081d0fb01 100644 --- a/testcases/verification/scala2013/ListOperations.scala +++ b/testcases/verification/scala2013/ListOperations.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/scala2013/PropositionalLogic.scala b/testcases/verification/scala2013/PropositionalLogic.scala index ca410a5ae541201b399dd680fc05a9427e9394ee..efc8f8f87b468b9b7a1283e3476a901e1cb32a2a 100644 --- a/testcases/verification/scala2013/PropositionalLogic.scala +++ b/testcases/verification/scala2013/PropositionalLogic.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/scala2013/RedBlackTree.scala b/testcases/verification/scala2013/RedBlackTree.scala index 11daef0b03ee0e4eae57db7735128456e3844649..a65cc1f0fac091ba639cdca983c3ccaeb2540ed8 100644 --- a/testcases/verification/scala2013/RedBlackTree.scala +++ b/testcases/verification/scala2013/RedBlackTree.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/scala2013/SearchLinkedList.scala b/testcases/verification/scala2013/SearchLinkedList.scala index 02f265f12b1c6cf6e12c0d6fcf5df6dbb3e71558..f85d51421fa5620105bf402021e95d997315977e 100644 --- a/testcases/verification/scala2013/SearchLinkedList.scala +++ b/testcases/verification/scala2013/SearchLinkedList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/vstte10competition/AmortizedQueue.scala b/testcases/verification/vstte10competition/AmortizedQueue.scala index 696d92c40592c7190bcf88ef5fe5cd80ccae80cd..4ba21d023bc9b47e26ad479b111396750829037a 100644 --- a/testcases/verification/vstte10competition/AmortizedQueue.scala +++ b/testcases/verification/vstte10competition/AmortizedQueue.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/vstte10competition/Injection.scala b/testcases/verification/vstte10competition/Injection.scala deleted file mode 100644 index 22b9d2d25c7f148b15b0f3c0e0c7a2df9a8941b0..0000000000000000000000000000000000000000 --- a/testcases/verification/vstte10competition/Injection.scala +++ /dev/null @@ -1,78 +0,0 @@ -import scala.collection.immutable.Set -import leon.lang._ -import leon.annotation._ - -object Injection { - sealed abstract class List - case class Cons(head : Int, tail : List) extends List - case class Nil() extends List - - sealed abstract class OptionInt - case class Some(value : Int) extends OptionInt - case class None() extends OptionInt - - def size(list : List) : Int = (list match { - case Nil() => 0 - case Cons(_, xs) => 1 + size(xs) - }) ensuring(_ >= 0) - - def content(list : List) : Set[Int] = list match { - case Nil() => Set.empty[Int] - case Cons(x, xs) => content(xs) ++ Set(x) - } - - def completeSet(n : Int) : Set[Int] = if(n <= 0) { - Set.empty[Int] - } else { - completeSet(n-1) ++ Set(n-1) - } - - def at(list : List, i : Int) : OptionInt = { - if(i < 0) None() else list match { - case Nil() => None() - case Cons(x, _) if i == 0 => Some(x) - case Cons(_, xs) => at(xs, i - 1) - } - } ensuring(res => (res == None()) == (i < 0 || i >= size(list))) - - def reverse(l: List) : List = reverse0(l, Nil()) - def reverse0(l1: List, l2: List) : List = (l1 match { - case Nil() => l2 - case Cons(x, xs) => reverse0(xs, Cons(x, l2)) - }) ensuring(res => - size(res) == size(l1) + size(l2) && - content(res) == content(l1) ++ content(l2)) - - def isPermutation(list : List, n : Int) : Boolean = { - n < 0 || (size(list) == n && content(list) == completeSet(n)) - } - def prop0(list : List, n : Int) : Boolean = { - require(n >= 0 && isPermutation(list, n)) - isPermutation(reverse(list), n) - } holds - - def indexOf(e : Int, list : List) : Int = (list match { - case Nil() => 0 - case Cons(x, xs) => if (x == e) 0 else 1 + indexOf(e, xs) - }) ensuring(res => (res == size(list)) == !content(list).contains(e)) - - // def invert(list : List, n : Int) : List = { - // require(isPermutation(list, n)) - // list - // } ensuring(res => isPermutation(res, n)) - - def f(list : List) = f0(list, size(list)-1, Nil()) - def f0(list : List, c : Int, acc : List) : List = { - require(isPermutation(list, size(list)) && c <= size(list)) - if(c < 0) { - acc - } else { - f0(list, c-1, Cons(indexOf(c, list), acc)) - } - } ensuring(res => content(acc) -- completeSet(n) == Set.empty) - - def main(args : Array[String]) : Unit = { - val test = Cons(9, Cons(3, Cons(8, Cons(2, Cons(7, Cons(4, Cons(0, Cons(1, Cons(5, Cons(6, Nil())))))))))) - println(f(test, size(test))) - } -} diff --git a/testcases/verification/vstte10competition/SearchLinkedList.scala b/testcases/verification/vstte10competition/SearchLinkedList.scala index 02f265f12b1c6cf6e12c0d6fcf5df6dbb3e71558..f85d51421fa5620105bf402021e95d997315977e 100644 --- a/testcases/verification/vstte10competition/SearchLinkedList.scala +++ b/testcases/verification/vstte10competition/SearchLinkedList.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.lang._ import leon.annotation._ diff --git a/testcases/verification/xlang/BinaryTreeImp.scala b/testcases/verification/xlang/BinaryTreeImp.scala index 57542971b6c05714a62cd75c667f1891c04c22ae..b731586da823e78bb590ecc92f856442f9f7ce2c 100644 --- a/testcases/verification/xlang/BinaryTreeImp.scala +++ b/testcases/verification/xlang/BinaryTreeImp.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/xlang/BubbleFun.scala b/testcases/verification/xlang/BubbleFun.scala index 4847fc8acf0e756b3af6d8f5bad84ff2c83b2406..a7c72648cd6c5ca3d26584ab33bcb6624d5e8432 100644 --- a/testcases/verification/xlang/BubbleFun.scala +++ b/testcases/verification/xlang/BubbleFun.scala @@ -1,3 +1,5 @@ +import leon.lang._ + object BubbleFun { // --------------------- sort ---------------------- diff --git a/testcases/verification/xlang/InsertionSortImp.scala b/testcases/verification/xlang/InsertionSortImp.scala index 67e37a68665e6b856be711395d4c4bd16fbb71fd..0a53cb55f4ef32b775646e1ea43a8c74b33a80c7 100644 --- a/testcases/verification/xlang/InsertionSortImp.scala +++ b/testcases/verification/xlang/InsertionSortImp.scala @@ -1,4 +1,3 @@ -import scala.collection.immutable.Set import leon.annotation._ import leon.lang._ diff --git a/testcases/verification/xlang/IntOperations.scala b/testcases/verification/xlang/IntOperations.scala index 98c9f9e5fdcc580de10a9e51060c5ab95a2eaff9..91b3b636c23c59c4bc1b7d313ef419e41e3b9912 100644 --- a/testcases/verification/xlang/IntOperations.scala +++ b/testcases/verification/xlang/IntOperations.scala @@ -1,3 +1,5 @@ +import leon.lang._ + object IntOperations { def sum(a: Int, b: Int) : Int = { require(b >= 0)