diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index c724f05b37aa67f0df165af330e37f6b9bb5d9de..70941a6861c2dd01c46da80e016894cd746684c1 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -134,7 +134,7 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
enumerationRelation = LessEquals, modularlyAnalyze, targettedUnroll, autoInference,
dumpStats, tightBounds, withmult, usereals, inferTemp, useCegis, timeout, maxCegisBound, statsSuff)
val report = (new InferenceEngine(inferctx)).run()
- println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
+ //println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
report
}
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index 15c1a1ffef4bbbc0d011431c3e915db8e3cf54e9..26337c6fff8111ba59f11dfd25213ee61610ac8b 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -20,13 +20,13 @@ class InferenceCondition(val invariant: Option[Expr], funDef: FunDef)
extends VC(BooleanLiteral(true), funDef, null) {
var time: Option[Double] = None
+ lazy val prettyInv = invariant.map(inv =>
+ simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv), fd)))
- def status: String = invariant match {
+ def status: String = prettyInv match {
case None => "unknown"
- case Some(inv) => {
- val prettyInv = simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv), fd))
- PrettyPrinter(prettyInv)
- }
+ case Some(inv) =>
+ PrettyPrinter(inv)
}
}
@@ -97,14 +97,13 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContex
val uninstFdOpt =
if (uninstFunName.isEmpty) None
else Util.functionByName(uninstFunName, ctx.uninstrumentedProgram)
- if (uninstFdOpt.isDefined) {
+ if (uninstFdOpt.isDefined) {
acc + (fd -> uninstFdOpt.get)
- }
- else acc
+ } else acc
}
val funToPost = conditions.collect {
case cd if cd.invariant.isDefined && funToUninstFun.contains(cd.fd) =>
- funToUninstFun(cd.fd) -> cd.invariant.get
+ funToUninstFun(cd.fd) -> cd.prettyInv.get
}.toMap
//println("Function to template: " + funToTmpl.map { case (k, v) => s"${k.id.name} --> $v" }.mkString("\n"))
Util.assignTemplateAndCojoinPost(Map(), ctx.uninstrumentedProgram, funToPost, uniqueIdDisplay = false)
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 5d6f7c0e728104475e2e29b5a92196f2ee6aca49..71531eeef02649facfbc439c95bf3c81e5b00ebb 100644
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
@@ -24,7 +24,7 @@ class OrbRegressionSuite extends LeonRegressionSuite {
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
val program = beginPipe.run(ctx)(f.getAbsolutePath :: Nil)
- val processPipe = InstrumentationPhase andThen InferInvariantsPhase
+ val processPipe = InferInvariantsPhase
val report = processPipe.run(ctx)(program)
val fails = report.conditions.filterNot(_.invariant.isDefined)
if (!fails.isEmpty)
diff --git a/testcases/web/invariant/01_Binary_Trie.scala b/testcases/web/invariant/01_Binary_Trie.scala
new file mode 100644
index 0000000000000000000000000000000000000000..38ff37b950b4229ba1ae17c959f75574ec00853b
--- /dev/null
+++ b/testcases/web/invariant/01_Binary_Trie.scala
@@ -0,0 +1,116 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object BinaryTrie {
+ sealed abstract class Tree
+ case class Leaf() extends Tree
+ case class Node(nvalue: BigInt, left: Tree, right: Tree) extends Tree
+
+ sealed abstract class IList
+ case class Cons(head: BigInt, tail: IList) extends IList
+ case class Nil() extends IList
+
+ def listSize(l: IList): BigInt = (l match {
+ case Nil() => 0
+ case Cons(x, xs) => 1 + listSize(xs)
+ })
+
+ def height(t: Tree): BigInt = {
+ t match {
+ case Leaf() => 0
+ case Node(x, l, r) => {
+ val hl = height(l)
+ val hr = height(r)
+ if (hl > hr) hl + 1 else hr + 1
+ }
+ }
+ }
+
+ def find(inp: IList, t: Tree): Tree = {
+ inp match {
+ case Nil() => t
+ case Cons(x, Nil()) => t
+ case Cons(x, xs @ Cons(y, _)) => {
+ t match {
+ case Leaf() => t
+ case Node(v, l, r) => {
+ if (y > 0) find(xs, l) else find(xs, r)
+ }
+ }
+ }
+ case _ => t
+ }
+ } ensuring (_ => time <= ? * listSize(inp) + ?)
+
+ def insert(inp: IList, t: Tree): Tree = {
+ t match {
+ case Leaf() => {
+ inp match {
+ case Nil() => t
+ case Cons(x, xs) => {
+ val newch = insert(xs, Leaf())
+ newch match {
+ case Leaf() => Node(x, Leaf(), Leaf())
+ case Node(y, _, _) => if (y > 0) Node(x, newch, Leaf()) else Node(y, Leaf(), newch)
+ }
+ }
+ }
+
+ }
+ case Node(v, l, r) => {
+ inp match {
+ case Nil() => t
+ case Cons(x, Nil()) => t
+ case Cons(x, xs @ Cons(y, _)) => {
+ val ch = if (y > 0) l else r
+ if (y > 0)
+ Node(v, insert(xs, ch), r)
+ else
+ Node(v, l, insert(xs, ch))
+ }
+ case _ => t
+ }
+ }
+ }
+ } ensuring (_ => time <= ? * listSize(inp) + ?)
+
+ def create(inp: IList): Tree = {
+ insert(inp, Leaf())
+ } ensuring (res => time <= ? * listSize(inp) + ?)
+
+ def delete(inp: IList, t: Tree): Tree = {
+ t match {
+ case Leaf() => {
+ inp match {
+ case Nil() => Leaf()
+ case Cons(x ,xs) => {
+ Leaf()
+ }
+ }
+ }
+ case Node(v, l, r) => {
+ inp match {
+ case Nil() => {
+ t
+ }
+ case Cons(x, Nil()) => {
+ if(l == Leaf() && r == Leaf()) Leaf()
+ else t
+ }
+ case Cons(x ,xs@Cons(y, _)) => {
+ val ch = if(y > 0) l else r
+ val newch = delete(xs, ch)
+ if(newch == Leaf() && ((y > 0 && r == Leaf()) || (y <= 0 && l == Leaf()))) Leaf()
+ else {
+ if(y > 0)
+ Node(v, newch, r)
+ else
+ Node(v, l, newch)
+ }
+ }
+ case _ => t
+ }
+ }
+ }
+ } ensuring (_ => time <= ? * listSize(inp) + ?)
+}
\ No newline at end of file
diff --git a/testcases/web/invariant/02_Binomial_Heap.scala b/testcases/web/invariant/02_Binomial_Heap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..905ab01461e0c8b6fd2558a6573e8a53f0b57c84
--- /dev/null
+++ b/testcases/web/invariant/02_Binomial_Heap.scala
@@ -0,0 +1,154 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object BinomialHeap {
+ case class TreeNode(rank: BigInt, elem: Element, children: BinomialHeap)
+ case class Element(n: BigInt)
+
+ sealed abstract class BinomialHeap
+ case class ConsHeap(head: TreeNode, tail: BinomialHeap) extends BinomialHeap
+ case class NilHeap() extends BinomialHeap
+
+ sealed abstract class List
+ case class NodeL(head: BinomialHeap, tail: List) extends List
+ case class NilL() extends List
+
+ sealed abstract class OptionalTree
+ case class Some(t : TreeNode) extends OptionalTree
+ case class None() extends OptionalTree
+
+ private def leq(a: Element, b: Element) : Boolean = {
+ a match {
+ case Element(a1) => {
+ b match {
+ case Element(a2) => {
+ if(a1 <= a2) true
+ else false
+ }
+ }
+ }
+ }
+ }
+
+ def isEmpty(t: BinomialHeap) = t match {
+ case ConsHeap(_,_) => false
+ case _ => true
+ }
+
+ def rank(t: TreeNode) : BigInt = t.rank
+
+ def root(t: TreeNode) : Element = t.elem
+
+ def link(t1: TreeNode, t2: TreeNode): TreeNode = {
+ if (leq(t1.elem, t2.elem)) {
+ TreeNode(t1.rank + 1, t1.elem, ConsHeap(t2, t1.children))
+ } else {
+ TreeNode(t1.rank + 1, t2.elem, ConsHeap(t1, t2.children))
+ }
+ }
+
+ def treeNum(h: BinomialHeap) : BigInt = {
+ h match {
+ case ConsHeap(head, tail) => 1 + treeNum(tail)
+ case _ => 0
+ }
+ }
+
+ def insTree(t: TreeNode, h: BinomialHeap) : BinomialHeap = {
+ h match {
+ case ConsHeap(head, tail) => {
+ if (rank(t) < rank(head)) {
+ ConsHeap(t, h)
+ } else if (rank(t) > rank(head)) {
+ ConsHeap(head, insTree(t,tail))
+ } else {
+ insTree(link(t,head), tail)
+ }
+ }
+ case _ => ConsHeap(t, NilHeap())
+ }
+ } ensuring(_ => time <= ? * treeNum(h) + ?)
+
+ def merge(h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
+ h1 match {
+ case ConsHeap(head1, tail1) => {
+ h2 match {
+ case ConsHeap(head2, tail2) => {
+ if (rank(head1) < rank(head2)) {
+ ConsHeap(head1, merge(tail1, h2))
+ } else if (rank(head2) < rank(head1)) {
+ ConsHeap(head2, merge(h1, tail2))
+ } else {
+ mergeWithCarry(link(head1, head2), tail1, tail2)
+ }
+ }
+ case _ => h1
+ }
+ }
+ case _ => h2
+ }
+ } ensuring(_ => time <= ? * treeNum(h1) + ? * treeNum(h2) + ?)
+
+ def mergeWithCarry(t: TreeNode, h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
+ h1 match {
+ case ConsHeap(head1, tail1) => {
+ h2 match {
+ case ConsHeap(head2, tail2) => {
+ if (rank(head1) < rank(head2)) {
+ if (rank(t) < rank(head1))
+ ConsHeap(t, ConsHeap(head1, merge(tail1, h2)))
+ else
+ mergeWithCarry(link(t, head1), tail1, h2)
+ } else if (rank(head2) < rank(head1)) {
+ if (rank(t) < rank(head2))
+ ConsHeap(t, ConsHeap(head2, merge(h1, tail2)))
+ else
+ mergeWithCarry(link(t, head2), h1, tail2)
+ } else {
+ ConsHeap(t, mergeWithCarry(link(head1, head2), tail1, tail2))
+ }
+ }
+ case _ => {
+ insTree(t, h1)
+ }
+ }
+ }
+ case _ => insTree(t, h2)
+ }
+ } ensuring (_ => time <= ? * treeNum(h1) + ? * treeNum(h2) + ?)
+
+ def removeMinTree(h: BinomialHeap): (OptionalTree, BinomialHeap) = {
+ h match {
+ case ConsHeap(head, NilHeap()) => (Some(head), NilHeap())
+ case ConsHeap(head1, tail1) => {
+ val (opthead2, tail2) = removeMinTree(tail1)
+ opthead2 match {
+ case Some(head2) =>
+ if (leq(root(head1), root(head2))) {
+ (Some(head1), tail1)
+ } else {
+ (Some(head2), ConsHeap(head1, tail2))
+ }
+ case _ => (Some(head1), tail1)
+ }
+ }
+ case _ => (None(), NilHeap())
+ }
+ } ensuring (res => treeNum(res._2) <= treeNum(h) && time <= ? * treeNum(h) + ?)
+
+ def minTreeChildren(h: BinomialHeap) : BigInt = {
+ val (min, _) = removeMinTree(h)
+ min match {
+ case Some(TreeNode(_,_,ch)) => treeNum(ch)
+ case _ => 0
+ }
+ }
+
+ def deleteMin(h: BinomialHeap) : BinomialHeap = {
+ val (min, ts2) = removeMinTree(h)
+ min match {
+ case Some(TreeNode(_,_,ts1)) => merge(ts1, ts2)
+ case _ => h
+ }
+ } ensuring(_ => time <= ? * minTreeChildren(h) + ? * treeNum(h) + ?)
+}
diff --git a/testcases/web/invariant/03_List_Concat.scala b/testcases/web/invariant/03_List_Concat.scala
new file mode 100644
index 0000000000000000000000000000000000000000..44b8e0fb239222cdf7f4263adcdfd25c40bcf076
--- /dev/null
+++ b/testcases/web/invariant/03_List_Concat.scala
@@ -0,0 +1,41 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object ConcatVariations {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ })
+
+ def genL(n: BigInt): List = {
+ require(n >= 0)
+ if (n == 0) Nil()
+ else
+ Cons(n, genL(n - 1))
+ } ensuring (res => size(res) == n && time <= ? *n + ?)
+
+ def append(l1: List, l2: List): List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => Cons(x, append(xs, l2))
+
+ }) ensuring (res => size(l1) + size(l2) == size(res) && time <= ? *size(l1) + ?)
+
+ def f_good(m: BigInt, n: BigInt): List = {
+ require(0 <= m && 0 <= n)
+ if (m == 0) Nil()
+ else append(genL(n), f_good(m - 1, n))
+
+ } ensuring(res => size(res) == n*m && time <= ? *(n*m) + ? *n + ? *m + ?)
+
+ def f_worst(m: BigInt, n: BigInt): List = {
+ require(0 <= m && 0 <= n)
+
+ if (m == 0) Nil()
+ else append(f_worst(m - 1, n), genL(n))
+
+ } ensuring(res => size(res) == n*m && time <= ? *((n*m)*m)+ ? *(n*m)+ ? *n+ ? *m+ ?)
+}
diff --git a/testcases/web/invariant/04_Red_Black_Tree.scala b/testcases/web/invariant/04_Red_Black_Tree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..43f3c7248bdc5a551d44fb5e6186109c7b1b3b4a
--- /dev/null
+++ b/testcases/web/invariant/04_Red_Black_Tree.scala
@@ -0,0 +1,108 @@
+import leon.invariant._
+import leon.instrumentation._
+import scala.collection.immutable.Set
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: BigInt, right: Tree) extends Tree
+
+ def twopower(x: BigInt) : BigInt = {
+ require(x >= 0)
+ if(x < 1) 1
+ else
+ 2* twopower(x - 1)
+ }
+
+ def size(t: Tree): BigInt = {
+ require(blackBalanced(t))
+ (t match {
+ case Empty() => BigInt(0)
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ })
+ } ensuring (res => twopower(blackHeight(t)) <= ? *res + ?)
+
+ def blackHeight(t : Tree) : BigInt = {
+ t match {
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ case _ => 0
+ }
+ }
+
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case _ => false
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case _ => true
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case _ => true
+ }
+
+ def ins(x: BigInt, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if(x < y) {
+ val t1 = ins(x, a)
+ balance(c, t1, y, b)
+ }
+ else if (x == y){
+ Node(c,a,y,b)
+ }
+ else{
+ val t1 = ins(x, b)
+ balance(c,a,y,t1)
+ }
+ }
+ } ensuring(res => time <= ? *blackHeight(t) + ?)
+
+ def makeBlack(n: Tree): Tree = {
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ }
+
+ def add(x: BigInt, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ val t1 = ins(x, t)
+ makeBlack(t1)
+
+ } ensuring(res => time <= ? *blackHeight(t) + ?)
+
+ def balance(co: Color, l: Tree, x: BigInt, r: Tree): Tree = {
+ Node(co,l,x,r)
+ match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case _ => Node(co,l,x,r)
+ }
+ }
+}
diff --git a/testcases/web/invariant/05_Leftist_Heap.scala b/testcases/web/invariant/05_Leftist_Heap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b938b3807fc4fcaf35c45bf43f74730aa8c565ca
--- /dev/null
+++ b/testcases/web/invariant/05_Leftist_Heap.scala
@@ -0,0 +1,82 @@
+import leon.invariant._
+import leon.instrumentation._
+import leon.annotation._
+
+object LeftistHeap {
+ sealed abstract class Heap
+ case class Leaf() extends Heap
+ case class Node(rk : BigInt, value: BigInt, left: Heap, right: Heap) extends Heap
+
+ private def rightHeight(h: Heap) : BigInt = h match {
+ case Leaf() => 0
+ case Node(_,_,_,r) => rightHeight(r) + 1
+ }
+
+ private def rank(h: Heap) : BigInt = h match {
+ case Leaf() => 0
+ case Node(rk,_,_,_) => rk
+ }
+
+ private def hasLeftistProperty(h: Heap) : Boolean = (h match {
+ case Leaf() => true
+ case Node(_,_,l,r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r) && (rank(h) == rightHeight(h))
+ })
+
+ @monotonic
+ def twopower(x: BigInt) : BigInt = {
+ require(x >= 0)
+ if(x < 1) 1
+ else
+ 2* twopower(x - 1)
+ }
+
+ def size(t: Heap): BigInt = {
+ require(hasLeftistProperty(t))
+ (t match {
+ case Leaf() => BigInt(0)
+ case Node(_,v, l, r) => size(l) + 1 + size(r)
+ })
+ } ensuring (res => twopower(rightHeight(t)) <= ? *res + ?)
+
+ def leftRightHeight(h: Heap) : BigInt = {h match {
+ case Leaf() => 0
+ case Node(_,_,l,r) => rightHeight(l)
+ }}
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h))
+ h match {
+ case Node(_,_,l,r) => merge(l, r)
+ case l @ Leaf() => l
+ }
+ } ensuring(res => time <= ? *leftRightHeight(h) + ?)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(hasLeftistProperty(h1) && hasLeftistProperty(h2))
+ h1 match {
+ case Leaf() => h2
+ case Node(_, v1, l1, r1) => h2 match {
+ case Leaf() => h1
+ case Node(_, v2, l2, r2) =>
+ if(v1 > v2)
+ makeT(v1, l1, merge(r1, h2))
+ else
+ makeT(v2, l2, merge(h1, r2))
+ }
+ }
+ } ensuring(res => time <= ? *rightHeight(h1) + ? *rightHeight(h2) + ?)
+
+ private def makeT(value: BigInt, left: Heap, right: Heap) : Heap = {
+ if(rank(left) >= rank(right))
+ Node(rank(right) + 1, value, left, right)
+ else
+ Node(rank(left) + 1, value, right, left)
+ }
+
+ def insert(element: BigInt, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap))
+
+ merge(Node(1, element, Leaf(), Leaf()), heap)
+
+ } ensuring(res => time <= ? *rightHeight(heap) + ?)
+}
diff --git a/testcases/web/invariant/06_String_Buffer.scala b/testcases/web/invariant/06_String_Buffer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c5f7dcf9015c5f576ae9d9a59a997f8e45ec9f32
--- /dev/null
+++ b/testcases/web/invariant/06_String_Buffer.scala
@@ -0,0 +1,63 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object StringBuffer {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ })
+
+ sealed abstract class StringBuffer
+ case class Chunk(str: List, next: StringBuffer) extends StringBuffer
+ case class Empty() extends StringBuffer
+
+ def length(sb: StringBuffer) : BigInt = sb match {
+ case Chunk(_, next) => 1 + length(next)
+ case _ => 0
+ }
+
+ def sizeBound(sb: StringBuffer, k: BigInt) : Boolean ={
+ sb match {
+ case Chunk(str, next) => size(str) <= k && sizeBound(next, k)
+ case _ => 0 <= k
+ }
+ }
+
+ def Equals(str1: List, str2: List, s1: StringBuffer, s2: StringBuffer, k: BigInt) : Boolean = {
+ require(sizeBound(s1, k) && sizeBound(s2, k) && size(str1) <= k && size(str2) <= k && k >= 0)
+
+ (str1, str2) match {
+ case (Cons(h1,t1), Cons(h2,t2)) => {
+
+ if(h1 != h2) false
+ else Equals(t1,t2, s1,s2, k)
+ }
+ case (Cons(_,_), Nil()) => {
+ s2 match {
+ case Chunk(str, next) => Equals(str1, str, s1, next, k)
+ case Empty() => false
+ }
+ }
+ case (Nil(), Cons(_,_)) => {
+ s1 match {
+ case Chunk(str, next) => Equals(str, str2, next, s2, k)
+ case Empty() => false
+ }
+ }
+ case _ =>{
+ (s1,s2) match {
+ case (Chunk(nstr1, next1),Chunk(nstr2, next2)) => Equals(nstr1, nstr2, next1, next2, k)
+ case (Empty(),Chunk(nstr2, next2)) => Equals(str1, nstr2, s1, next2, k)
+ case (Chunk(nstr1, next1), Empty()) => Equals(nstr1, str2, next1, s2, k)
+ case _ => true
+ }
+ }
+ }
+ } ensuring(res => true && tmpl((a,b,c,d,e) => time <= a*((k+1)*(length(s1) + length(s2))) + b*size(str1) + e))
+
+ def max(x: BigInt, y: BigInt) : BigInt = if(x >= y) x else y
+}