Skip to content
Snippets Groups Projects
Commit bdbe4d98 authored by ravi's avatar ravi
Browse files

Fixing a compilation error in a web benchmark

parent 7ad3cdc6
No related branches found
No related tags found
No related merge requests found
...@@ -43,7 +43,7 @@ object TreeOperations { ...@@ -43,7 +43,7 @@ object TreeOperations {
case Node(l, x, r) => if (x <= elem) Node(l, x, insert(elem, r)) case Node(l, x, r) => if (x <= elem) Node(l, x, insert(elem, r))
else Node(insert(elem, l), x, r) else Node(insert(elem, l), x, r)
} }
} ensuring (res => height(res) <= height(t) + 1time <= ? *height(t) + ?) } ensuring (res => height(res) <= height(t) + 1 && time <= ? *height(t) + ?)
def addAll(l: List, t: Tree): Tree = { def addAll(l: List, t: Tree): Tree = {
l match { l match {
...@@ -53,7 +53,7 @@ object TreeOperations { ...@@ -53,7 +53,7 @@ object TreeOperations {
addAll(xs, newt) addAll(xs, newt)
} }
} }
} ensuring(res => tmpl((a,b,c) => time <= ? *(listSize(l) * (height(t) + listSize(l))) + ? *listSize(l) + ?) } ensuring(_ => time <= ? *(listSize(l) * (height(t) + listSize(l))) + ? *listSize(l) + ?)
def remove(elem: BigInt, t: Tree): Tree = { def remove(elem: BigInt, t: Tree): Tree = {
t match { t match {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment