From b4bd39dd4dd628340af4ad919731a21c722a0db1 Mon Sep 17 00:00:00 2001 From: ravi <ravi.kandhadai@epfl.ch> Date: Wed, 23 Dec 2015 17:52:36 +0100 Subject: [PATCH] Minor reorganization, and implementing trace-induct tactic --- leon.out/Conqueue-edited.scala | 2 + library/annotation/package.scala | 2 + library/lazy/package.scala | 11 ++++++ .../verification/TraceInductionTactic.scala | 38 +++++++++++++++++++ .../lazy-datastructures/LazyMegeSort.scala | 4 +- .../{ => Unproved}/FibonacciMemoized.scala | 3 +- .../{ => Unproved}/HammingProblem.scala | 4 +- .../{ => Unproved}/ImplicitQueue.scala | 1 + .../{ => conc}/ConcTrees.scala | 0 .../{ => conc}/Conqueue.scala | 7 ++-- 10 files changed, 63 insertions(+), 9 deletions(-) create mode 100644 src/main/scala/leon/verification/TraceInductionTactic.scala rename testcases/lazy-datastructures/{ => Unproved}/FibonacciMemoized.scala (95%) rename testcases/lazy-datastructures/{ => Unproved}/HammingProblem.scala (97%) rename testcases/lazy-datastructures/{ => Unproved}/ImplicitQueue.scala (99%) rename testcases/lazy-datastructures/{ => conc}/ConcTrees.scala (100%) rename testcases/lazy-datastructures/{ => conc}/Conqueue.scala (99%) diff --git a/leon.out/Conqueue-edited.scala b/leon.out/Conqueue-edited.scala index 10ebf9aaa..3e9ba4df1 100644 --- a/leon.out/Conqueue-edited.scala +++ b/leon.out/Conqueue-edited.scala @@ -7,6 +7,8 @@ import leon.lang.synthesis._ import ConcTrees._ import ConQ._ import Conqueue._ +import conc.Conqueue +import conc.ConcTrees object ConcTrees { abstract class Conc[T] { diff --git a/library/annotation/package.scala b/library/annotation/package.scala index c65c16926..a473add82 100644 --- a/library/annotation/package.scala +++ b/library/annotation/package.scala @@ -10,6 +10,8 @@ package object annotation { @ignore class induct extends StaticAnnotation @ignore + class traceInduct extends StaticAnnotation + @ignore class ignore extends StaticAnnotation @ignore class extern extends StaticAnnotation diff --git a/library/lazy/package.scala b/library/lazy/package.scala index 2a6a29cf2..f64cec654 100644 --- a/library/lazy/package.scala +++ b/library/lazy/package.scala @@ -5,6 +5,7 @@ package leon.lazyeval import leon.annotation._ import leon.lang._ import scala.language.implicitConversions +import scala.annotation.StaticAnnotation @library object $ { @@ -48,6 +49,16 @@ object $ { @inline implicit def toWithState[T](x: T) = new WithState(x) + + /** + * annotations for monotonicity proofs. + * Note implemented as of now. + * Let foo be the method that has the annotation. + * The given name `methodname` should have the following form: + * m(arg1, ..., argn, substate-Set1,..., substate-Setn, superstate-Set1, ..., superstate-Setn) + */ + @ignore + class monoproof(methodname: String) extends StaticAnnotation } @library diff --git a/src/main/scala/leon/verification/TraceInductionTactic.scala b/src/main/scala/leon/verification/TraceInductionTactic.scala new file mode 100644 index 000000000..138148231 --- /dev/null +++ b/src/main/scala/leon/verification/TraceInductionTactic.scala @@ -0,0 +1,38 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + +package leon +package verification + +import purescala.Definitions._ +import purescala.Expressions._ + +/** + * This tactic applies only to non-recursive functions. + * Inducts over the recursive calls of the first recursive procedure, in the body of `funDef` + */ +class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) { + val description : String = + + implicit protected val ctx = vctx.context + + def generateVCs(fd: FunDef): Seq[VC] = { + generatePostconditions(fd) ++ + generatePreconditions(fd) ++ + generateCorrectnessConditions(fd) + } + + def generatePostconditions(function: FunDef): Seq[VC] + def generatePreconditions(function: FunDef): Seq[VC] + def generateCorrectnessConditions(function: FunDef): Seq[VC] + + protected def sizeLimit(s: String, limit: Int) = { + require(limit > 3) + // Crop the call to display it properly + val res = s.takeWhile(_ != '\n').take(limit) + if (res == s) { + res + } else { + res + " ..." + } + } +} diff --git a/testcases/lazy-datastructures/LazyMegeSort.scala b/testcases/lazy-datastructures/LazyMegeSort.scala index 503dc8cb5..9ddca941e 100644 --- a/testcases/lazy-datastructures/LazyMegeSort.scala +++ b/testcases/lazy-datastructures/LazyMegeSort.scala @@ -54,9 +54,7 @@ object MergeSort { } ensuring (res => res._2.size == l.size - n && res._1.size == n && stack <= 25 * l.size - 1) /* - * Note: merge is not recursive due to closures. - * However, concretizing merge may invoke merge or msort recursively. - * So proving standalone bound for merge requires preconditions. + * Proving standalone bound for merge requires preconditions. */ def merge(a: $[LList], b: $[LList]): LList = (b.value match { case SNil() => a.value diff --git a/testcases/lazy-datastructures/FibonacciMemoized.scala b/testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala similarity index 95% rename from testcases/lazy-datastructures/FibonacciMemoized.scala rename to testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala index 34490f82f..385c1498f 100644 --- a/testcases/lazy-datastructures/FibonacciMemoized.scala +++ b/testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala @@ -1,9 +1,10 @@ -package lazybenchmarks +package Unproved import leon.lazyeval._ import leon.lang._ import leon.annotation._ import leon.instrumentation._ +import scala.math.BigInt.int2bigInt //import leon.invariant._ object FibMem { diff --git a/testcases/lazy-datastructures/HammingProblem.scala b/testcases/lazy-datastructures/Unproved/HammingProblem.scala similarity index 97% rename from testcases/lazy-datastructures/HammingProblem.scala rename to testcases/lazy-datastructures/Unproved/HammingProblem.scala index 18ee1207a..79acc3ba6 100644 --- a/testcases/lazy-datastructures/HammingProblem.scala +++ b/testcases/lazy-datastructures/Unproved/HammingProblem.scala @@ -1,9 +1,9 @@ -package lazybenchmarks - import leon.lazyeval._ import leon.lang._ import leon.annotation._ import leon.instrumentation._ +import leon.lazyeval.$.eagerToLazy +import scala.math.BigInt.int2bigInt //import leon.invariant._ /** diff --git a/testcases/lazy-datastructures/ImplicitQueue.scala b/testcases/lazy-datastructures/Unproved/ImplicitQueue.scala similarity index 99% rename from testcases/lazy-datastructures/ImplicitQueue.scala rename to testcases/lazy-datastructures/Unproved/ImplicitQueue.scala index b69988cd5..61f6302a1 100644 --- a/testcases/lazy-datastructures/ImplicitQueue.scala +++ b/testcases/lazy-datastructures/Unproved/ImplicitQueue.scala @@ -3,6 +3,7 @@ import leon.lazyeval.$._ import leon.lang._ import leon.annotation._ import leon.instrumentation._ +import scala.math.BigInt.int2bigInt /** * This is an version of the implicit recursive slowdwon queues of diff --git a/testcases/lazy-datastructures/ConcTrees.scala b/testcases/lazy-datastructures/conc/ConcTrees.scala similarity index 100% rename from testcases/lazy-datastructures/ConcTrees.scala rename to testcases/lazy-datastructures/conc/ConcTrees.scala diff --git a/testcases/lazy-datastructures/Conqueue.scala b/testcases/lazy-datastructures/conc/Conqueue.scala similarity index 99% rename from testcases/lazy-datastructures/Conqueue.scala rename to testcases/lazy-datastructures/conc/Conqueue.scala index 7579f6dfe..80d77d21d 100644 --- a/testcases/lazy-datastructures/Conqueue.scala +++ b/testcases/lazy-datastructures/conc/Conqueue.scala @@ -1,4 +1,4 @@ -package lazybenchmarks +package conc import leon.lazyeval._ import leon.lang._ @@ -7,6 +7,9 @@ import leon.annotation._ import leon.instrumentation._ import leon.lazyeval.$._ +import ConcTrees._ +import scala.math.BigInt.int2bigInt + object ConcTrees { sealed abstract class Conc[T] { @@ -30,8 +33,6 @@ object ConcTrees { case class Single[T](x: T) extends Conc[T] case class CC[T](left: Conc[T], right: Conc[T]) extends Conc[T] } - -import ConcTrees._ object Conqueue { sealed abstract class ConQ[T] { -- GitLab