Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
leon-repair [2015/02/09 03:13] ekneuss |
leon-repair [2015/02/10 17:14] ekneuss |
||
---|---|---|---|
Line 38: | Line 38: | ||
* [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/PropLogic/PropLogic4.scala|PropLogic.nnf4]] | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/PropLogic/PropLogic4.scala|PropLogic.nnf4]] | ||
* [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/PropLogic/PropLogic5.scala|PropLogic.nnf5]] | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/PropLogic/PropLogic5.scala|PropLogic.nnf5]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/Numerical/Numerical1.scala|Numerical.power]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/Numerical/Numerical3.scala|Numerical.moddiv]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/MergeSort/MergeSort1.scala|MergeSort.split]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/MergeSort/MergeSort2.scala|MergeSort.merge1]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/MergeSort/MergeSort3.scala|MergeSort.merge2]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/MergeSort/MergeSort4.scala|MergeSort.merge3]] | ||
+ | * [[https://github.com/colder/leon/blob/topic/repair/testcases/repair/MergeSort/MergeSort5.scala|MergeSort.merge4]] | ||
+ | |||
+ | The version of Leon used to run all these benchmarks is [[https://github.com/colder/leon/tree/ddd08e3aac4cc52c51dc60b59867eaea38f3cbf5| publicly available on Github]]. | ||
+ | |||
+ | |||
+ | The following output is produced by the tool: | ||
+ | |||
+ | %%% Compiler1.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def desugar(e : Trees.Expr): SimpleE = { | ||
+ | e match { | ||
+ | case Trees.Plus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Minus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), Neg(desugar(rhs))) | ||
+ | case Trees.LessThan(lhs, rhs) => | ||
+ | LessThan(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.And(lhs, rhs) => | ||
+ | Ite(desugar(lhs), desugar(rhs), Literal(0)) | ||
+ | case Trees.Or(lhs, rhs) => | ||
+ | Ite(desugar(lhs), Literal(1), desugar(rhs)) | ||
+ | case Trees.Not(e) => | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | case Trees.Eq(lhs, rhs) => | ||
+ | Eq(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Ite(cond, thn, els) => | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | case Trees.IntLiteral(v) => | ||
+ | Literal(v) | ||
+ | case Trees.BoolLiteral(b) => | ||
+ | Literal(b2i(b)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : SimpleE) => (e, res) passes { | ||
+ | case Trees.Plus(Trees.IntLiteral(i), Trees.Minus(Trees.IntLiteral(j), Trees.IntLiteral(42))) => | ||
+ | Plus(Literal(i), Plus(Literal(j), Neg(Literal(42)))) | ||
+ | } && sem(res) == semUntyped(e) | ||
+ | } | ||
+ | |||
+ | %%% Compiler2.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Plus(None[SimpleE]().getOrElse(desugar(lhs)), Neg(desugar(rhs))) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def desugar(e : Trees.Expr): SimpleE = { | ||
+ | e match { | ||
+ | case Trees.Plus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Minus(lhs, rhs) => | ||
+ | Plus(None[SimpleE]().getOrElse(desugar(lhs)), Neg(desugar(rhs))) | ||
+ | case Trees.LessThan(lhs, rhs) => | ||
+ | LessThan(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.And(lhs, rhs) => | ||
+ | Ite(desugar(lhs), desugar(rhs), Literal(0)) | ||
+ | case Trees.Or(lhs, rhs) => | ||
+ | Ite(desugar(lhs), Literal(1), desugar(rhs)) | ||
+ | case Trees.Not(e) => | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | case Trees.Eq(lhs, rhs) => | ||
+ | Eq(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Ite(cond, thn, els) => | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | case Trees.IntLiteral(v) => | ||
+ | Literal(v) | ||
+ | case Trees.BoolLiteral(b) => | ||
+ | Literal(b2i(b)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : SimpleE) => sem(res) == semUntyped(e) && (e, res) passes { | ||
+ | case Trees.Minus(Trees.IntLiteral(42), Trees.IntLiteral(i)) => | ||
+ | Plus(Literal(42), Neg(Literal(i))) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% Compiler3.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def desugar(e : Trees.Expr): SimpleE = { | ||
+ | e match { | ||
+ | case Trees.Plus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Minus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), Neg(desugar(rhs))) | ||
+ | case Trees.LessThan(lhs, rhs) => | ||
+ | LessThan(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.And(lhs, rhs) => | ||
+ | Ite(desugar(lhs), desugar(rhs), Literal(0)) | ||
+ | case Trees.Or(lhs, rhs) => | ||
+ | Ite(desugar(lhs), Literal(1), desugar(rhs)) | ||
+ | case Trees.Not(e) => | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | case Trees.Eq(lhs, rhs) => | ||
+ | Eq(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Ite(cond, thn, els) => | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | case Trees.IntLiteral(v) => | ||
+ | Literal(v) | ||
+ | case Trees.BoolLiteral(b) => | ||
+ | Literal(b2i(b)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : SimpleE) => sem(res) == semUntyped(e) | ||
+ | } | ||
+ | |||
+ | %%% Compiler4.scala | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def desugar(e : Trees.Expr): SimpleE = { | ||
+ | e match { | ||
+ | case Trees.Plus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Minus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), Neg(desugar(rhs))) | ||
+ | case Trees.LessThan(lhs, rhs) => | ||
+ | LessThan(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.And(lhs, rhs) => | ||
+ | Ite(desugar(lhs), desugar(rhs), Literal(0)) | ||
+ | case Trees.Or(lhs, rhs) => | ||
+ | Ite(desugar(lhs), Literal(1), desugar(rhs)) | ||
+ | case Trees.Not(e) => | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | case Trees.Eq(lhs, rhs) => | ||
+ | Eq(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Ite(cond, thn, els) => | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | case Trees.IntLiteral(v) => | ||
+ | Literal(v) | ||
+ | case Trees.BoolLiteral(b) => | ||
+ | Literal(b2i(b)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : SimpleE) => sem(res) == semUntyped(e) | ||
+ | } | ||
+ | |||
+ | %%% Compiler5.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | e match { | ||
+ | case Plus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | case Minus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), Neg(desugar(rhs))) | ||
+ | case LessThan(lhs, rhs) => | ||
+ | LessThan(desugar(lhs), desugar(rhs)) | ||
+ | case And(lhs, rhs) => | ||
+ | Ite(desugar(lhs), desugar(rhs), Literal(0)) | ||
+ | case Or(lhs, rhs) => | ||
+ | Ite(desugar(lhs), Literal(1), desugar(rhs)) | ||
+ | case Not(e) => | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | case Eq(lhs, rhs) => | ||
+ | Eq(desugar(lhs), desugar(rhs)) | ||
+ | case Ite(cond, thn, els) => | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | case IntLiteral(v) => | ||
+ | Literal(v) | ||
+ | case BoolLiteral(b) => | ||
+ | Literal(b2i(b)) | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def desugar(e : Trees.Expr): SimpleE = { | ||
+ | e match { | ||
+ | case Trees.Plus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Minus(lhs, rhs) => | ||
+ | Plus(desugar(lhs), Neg(desugar(rhs))) | ||
+ | case Trees.LessThan(lhs, rhs) => | ||
+ | LessThan(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.And(lhs, rhs) => | ||
+ | Ite(desugar(lhs), desugar(rhs), Literal(0)) | ||
+ | case Trees.Or(lhs, rhs) => | ||
+ | Ite(desugar(lhs), Literal(1), desugar(rhs)) | ||
+ | case Trees.Not(e) => | ||
+ | Ite(desugar(e), Literal(0), Literal(1)) | ||
+ | case Trees.Eq(lhs, rhs) => | ||
+ | Eq(desugar(lhs), desugar(rhs)) | ||
+ | case Trees.Ite(cond, thn, els) => | ||
+ | Ite(desugar(cond), desugar(thn), desugar(els)) | ||
+ | case Trees.IntLiteral(v) => | ||
+ | Literal(v) | ||
+ | case Trees.BoolLiteral(b) => | ||
+ | Literal(b2i(b)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : SimpleE) => sem(res) == semUntyped(e) | ||
+ | } | ||
+ | |||
+ | %%% Compiler6.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | IntLiteral(a + b) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def simplify(e : Trees.Expr): Trees.Expr = { | ||
+ | e match { | ||
+ | case Trees.And(Trees.BoolLiteral(false), _) => | ||
+ | Trees.BoolLiteral(false) | ||
+ | case Trees.Or(Trees.BoolLiteral(true), _) => | ||
+ | Trees.BoolLiteral(true) | ||
+ | case Trees.Plus(Trees.IntLiteral(a), Trees.IntLiteral(b)) => | ||
+ | Trees.IntLiteral(a + b) | ||
+ | case Trees.Not(Trees.Not(Trees.Not(a))) => | ||
+ | Trees.Not(a) | ||
+ | case e => | ||
+ | e | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Trees.Expr) => eval(res) == eval(e) | ||
+ | } | ||
+ | |||
+ | %%% Compiler7.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | BoolLiteral(true) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | @induct | ||
+ | def simplify(e : Trees.Expr): Trees.Expr = { | ||
+ | e match { | ||
+ | case Trees.And(Trees.BoolLiteral(false), _) => | ||
+ | Trees.BoolLiteral(false) | ||
+ | case Trees.Or(Trees.BoolLiteral(true), _) => | ||
+ | Trees.BoolLiteral(true) | ||
+ | case Trees.Plus(Trees.IntLiteral(a), Trees.IntLiteral(b)) => | ||
+ | Trees.IntLiteral(a + b) | ||
+ | case Trees.Not(Trees.Not(Trees.Not(a))) => | ||
+ | Trees.Not(a) | ||
+ | case e => | ||
+ | e | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Trees.Expr) => eval(res) == eval(e) && (e, res) passes { | ||
+ | case Trees.Or(Trees.BoolLiteral(true), e) => | ||
+ | Trees.BoolLiteral(true) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% Heap1.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | v2 >= v1 | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(h1 : Heap, h2 : Heap): Heap = { | ||
+ | require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2)) | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v2 >= v1) { | ||
+ | makeN(v2, l2, merge(h1, r2)) | ||
+ | } else { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content() | ||
+ | } | ||
+ | |||
+ | %%% Heap2.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | h1 | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(h1 : Heap, h2 : Heap): Heap = { | ||
+ | require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2)) | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v1 >= v2) { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } else { | ||
+ | makeN(v2, l2, merge(h1, r2)) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content() | ||
+ | } | ||
+ | |||
+ | %%% Heap3.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | v2 <= v1 | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(h1 : Heap, h2 : Heap): Heap = { | ||
+ | require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2)) | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v2 <= v1) { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } else { | ||
+ | makeN(v2, l2, merge(h1, r2)) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content() | ||
+ | } | ||
+ | |||
+ | %%% Heap4.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | makeN(v2, l2, merge(h1, r2)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(h1 : Heap, h2 : Heap): Heap = { | ||
+ | require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2)) | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v1 >= v2) { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } else { | ||
+ | makeN(v2, l2, merge(h1, r2)) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content() | ||
+ | } | ||
+ | |||
+ | %%% Heap5.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | v1 + v2 > v2 + v2 | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(h1 : Heap, h2 : Heap): Heap = { | ||
+ | require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2)) | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v1 + v2 > v2 + v2) { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } else { | ||
+ | makeN(v2, l2, merge(h1, r2)) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content() | ||
+ | } | ||
+ | |||
+ | %%% Heap6.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | merge(Node(element, Leaf(), Leaf()), heap) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def insert(element : Int, heap : Heap): Heap = { | ||
+ | require(hasLeftistProperty(heap) && hasHeapProperty(heap)) | ||
+ | merge(Node(element, Leaf(), Leaf()), heap) | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(res) == heapSize(heap) + 1 && res.content() == heap.content() ++ Set[Int](element) | ||
+ | } | ||
+ | |||
+ | %%% Heap7.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | left.rank() >= right.rank() | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def makeN(value : Int, left : Heap, right : Heap): Heap = { | ||
+ | require(hasLeftistProperty(left) && hasLeftistProperty(right)) | ||
+ | if (left.rank() >= right.rank()) { | ||
+ | Node(value, left, right) | ||
+ | } else { | ||
+ | Node(value, right, left) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) | ||
+ | } | ||
+ | |||
+ | Solution is not trusted! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v1 >= v2) { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } else { | ||
+ | makeN(v2, merge(h1, r2), l2) | ||
+ | } | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(h1 : Heap, h2 : Heap): Heap = { | ||
+ | require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2)) | ||
+ | (h1, h2) match { | ||
+ | case (Leaf(), _) => | ||
+ | h2 | ||
+ | case (_, Leaf()) => | ||
+ | h1 | ||
+ | case (Node(v1, l1, r1), Node(v2, l2, r2)) => | ||
+ | if (v1 >= v2) { | ||
+ | makeN(v1, l1, merge(r1, h2)) | ||
+ | } else { | ||
+ | makeN(v2, merge(h1, r2), l2) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content() | ||
+ | } | ||
+ | |||
+ | %%% PropLogic1.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | nnf(Not(e)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def nnf(formula : Formula): Formula = { | ||
+ | formula match { | ||
+ | case Not(And(lhs, rhs)) => | ||
+ | Or(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Or(lhs, rhs)) => | ||
+ | And(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Const(v)) => | ||
+ | Const(!v) | ||
+ | case Not(Not(e)) => | ||
+ | nnf(Not(e)) | ||
+ | case And(lhs, rhs) => | ||
+ | And(nnf(lhs), nnf(rhs)) | ||
+ | case Or(lhs, rhs) => | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | case other => | ||
+ | other | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Formula) => isNNF(res) && (formula, res) passes { | ||
+ | case Not(Not(Not(Const(a)))) => | ||
+ | Const(!a) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% PropLogic2.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | other match { | ||
+ | case Const(v) => | ||
+ | Literal(1) | ||
+ | case Literal(id) => | ||
+ | Const(false) | ||
+ | case Not(f) => | ||
+ | nnf(f) | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def nnf(formula : Formula): Formula = { | ||
+ | formula match { | ||
+ | case Not(And(lhs, rhs)) => | ||
+ | Or(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Or(lhs, rhs)) => | ||
+ | And(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Const(v)) => | ||
+ | Const(!v) | ||
+ | case And(lhs, rhs) => | ||
+ | And(nnf(lhs), nnf(rhs)) | ||
+ | case Or(lhs, rhs) => | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | case other => | ||
+ | other match { | ||
+ | case Const(v) => | ||
+ | Literal(1) | ||
+ | case Literal(id) => | ||
+ | Const(false) | ||
+ | case Not(f) => | ||
+ | nnf(f) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Formula) => isNNF(res) && (formula, res) passes { | ||
+ | case Not(Not(Not(Const(a)))) => | ||
+ | Const(!a) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% PropLogic3.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Const(false == v) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def nnf(formula : Formula): Formula = { | ||
+ | formula match { | ||
+ | case Not(And(lhs, rhs)) => | ||
+ | Or(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Or(lhs, rhs)) => | ||
+ | And(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Const(v)) => | ||
+ | Const(false == v) | ||
+ | case Not(Not(e)) => | ||
+ | nnf(e) | ||
+ | case And(lhs, rhs) => | ||
+ | And(nnf(lhs), nnf(rhs)) | ||
+ | case Or(lhs, rhs) => | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | case other => | ||
+ | other | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Formula) => isNNF(res) && (formula, res) passes { | ||
+ | case Not(Const(true)) => | ||
+ | Const(false) | ||
+ | case Not(Const(false)) => | ||
+ | Const(true) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% PropLogic4.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def nnf(formula : Formula): Formula = { | ||
+ | formula match { | ||
+ | case Not(And(lhs, rhs)) => | ||
+ | Or(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Or(lhs, rhs)) => | ||
+ | And(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Const(v)) => | ||
+ | Const(!v) | ||
+ | case Not(Not(e)) => | ||
+ | nnf(e) | ||
+ | case And(lhs, rhs) => | ||
+ | And(nnf(lhs), nnf(rhs)) | ||
+ | case Or(lhs, rhs) => | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | case other => | ||
+ | other | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Formula) => isNNF(res) && (formula, res) passes { | ||
+ | case Or(Not(Const(c)), Not(Literal(l))) => | ||
+ | Or(Const(!c), Not(Literal(l))) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% PropLogic5.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def nnf(formula : Formula): Formula = { | ||
+ | formula match { | ||
+ | case Not(And(lhs, rhs)) => | ||
+ | Or(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Or(lhs, rhs)) => | ||
+ | And(nnf(Not(lhs)), nnf(Not(rhs))) | ||
+ | case Not(Const(v)) => | ||
+ | Const(!v) | ||
+ | case Not(Not(e)) => | ||
+ | nnf(e) | ||
+ | case And(lhs, rhs) => | ||
+ | And(nnf(lhs), nnf(rhs)) | ||
+ | case Or(lhs, rhs) => | ||
+ | Or(nnf(lhs), nnf(rhs)) | ||
+ | case other => | ||
+ | other | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Formula) => isNNF(res) && (formula, res) passes { | ||
+ | case Or(Not(Const(c)), Not(Literal(l))) => | ||
+ | Or(Const(!c), Not(Literal(l))) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List1.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Cons0[T](h, t.pad(s, e)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$pad[T]($this : List0[T], s : Int, e : T): List0[T] = { | ||
+ | ($this, s) match { | ||
+ | case (_, s) if s <= 0 => | ||
+ | $this | ||
+ | case (Nil0(), s) => | ||
+ | Cons0[T](e, Nil0[T]().pad(s - 1, e)) | ||
+ | case (Cons0(h, t), s) => | ||
+ | Cons0[T](h, t.pad(s, e)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List0[T]) => (($this, s, e), res) passes { | ||
+ | case (Cons0(a, Nil0()), 2, x) => | ||
+ | Cons0[T](a, Cons0[T](x, Cons0[T](x, Nil0[T]()))) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List2.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Cons0[T](x, xs ++ that) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$$plus$plus[T]($this : List0[T], that : List0[T]): List0[T] = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | that | ||
+ | case Cons0(x, xs) => | ||
+ | Cons0[T](x, xs ++ that) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List0[T]) => res.content() == $this.content() ++ that.content() && res.size() == $this.size() + that.size() | ||
+ | } | ||
+ | |||
+ | %%% List3.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Cons0[T](t, Nil0[T]()) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$ap[T]($this : List0[T], t : T): List0[T] = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | Cons0[T](t, Nil0[T]()) | ||
+ | case Cons0(x, xs) => | ||
+ | Cons0[T](x, xs.ap(t)) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List0[T]) => res.size() == $this.size() + 1 && res.content() == $this.content() ++ Set[T](t) | ||
+ | } | ||
+ | |||
+ | %%% List4.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | if (h == from) { | ||
+ | Cons0[T](to, t.replace(h, to)) | ||
+ | } else { | ||
+ | Cons0[T](h, r) | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$replace[T]($this : List0[T], from : T, to : T): List0[T] = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | Nil0[T]() | ||
+ | case Cons0(h, t) => | ||
+ | val r = t.replace(from, to); | ||
+ | if (h == from) { | ||
+ | Cons0[T](to, t.replace(h, to)) | ||
+ | } else { | ||
+ | Cons0[T](h, r) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List0[T]) => $this.content() -- Set[T](from) ++ (if ($this.content().contains(e)) { | ||
+ | Set[T](to) | ||
+ | } else { | ||
+ | Set[T]() | ||
+ | }) == res.content() && res.size() == $this.size() | ||
+ | } | ||
+ | |||
+ | %%% List5.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | t.count(h) + 1 | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$count[T]($this : List0[T], e : T): Int = { | ||
+ | $this match { | ||
+ | case Cons0(h, t) => | ||
+ | if (h == e) { | ||
+ | t.count(h) + 1 | ||
+ | } else { | ||
+ | t.count(e) | ||
+ | } | ||
+ | case Nil0() => | ||
+ | 0 | ||
+ | } | ||
+ | } ensuring { | ||
+ | (x$2 : Int) => (($this, e), x$2) passes { | ||
+ | case (Cons0(a, Cons0(b, Cons0(a1, Cons0(b2, Nil0())))), a2) if a == a1 && a == a2 && b != a2 && b2 != a2 => | ||
+ | 2 | ||
+ | case (Cons0(a, Cons0(b, Nil0())), c) if a != c && b != c => | ||
+ | 0 | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List6.scala %%% | ||
+ | Solution is not trusted! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Some[Int](i + 1) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$find[T]($this : List0[T], e : T): Option[Int] = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | None[Int]() | ||
+ | case Cons0(h, t) => | ||
+ | if (h == e) { | ||
+ | Some[Int](0) | ||
+ | } else { | ||
+ | t.find(e) match { | ||
+ | case None() => | ||
+ | None[Int]() | ||
+ | case Some(i) => | ||
+ | Some[Int](i + 1) | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Option[Int]) => if ($this.content().contains(e)) { | ||
+ | res.isDefined() && $this.size() > res.get() && $this.apply(res.get()) == e | ||
+ | } else { | ||
+ | res.isEmpty() | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List7.scala %%% | ||
+ | Solution is not trusted! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Some[Int]((i + 2) - 1) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$find[T]($this : List0[T], e : T): Option[Int] = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | None[Int]() | ||
+ | case Cons0(h, t) => | ||
+ | if (h == e) { | ||
+ | Some[Int](0) | ||
+ | } else { | ||
+ | t.find(e) match { | ||
+ | case None() => | ||
+ | None[Int]() | ||
+ | case Some(i) => | ||
+ | Some[Int]((i + 2) - 1) | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Option[Int]) => if ($this.content().contains(e)) { | ||
+ | res.isDefined() && $this.size() > res.get() && $this.apply(res.get()) == e | ||
+ | } else { | ||
+ | res.isEmpty() | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List8.scala %%% | ||
+ | Solution is not trusted! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | if (e == h) { | ||
+ | Some[Int](0) | ||
+ | } else { | ||
+ | t.find(e) match { | ||
+ | case None() => | ||
+ | None[Int]() | ||
+ | case Some(i) => | ||
+ | Some[Int](i + 1) | ||
+ | } | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$find[T]($this : List0[T], e : T): Option[Int] = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | None[Int]() | ||
+ | case Cons0(h, t) => | ||
+ | if (e == h) { | ||
+ | Some[Int](0) | ||
+ | } else { | ||
+ | t.find(e) match { | ||
+ | case None() => | ||
+ | None[Int]() | ||
+ | case Some(i) => | ||
+ | Some[Int](i + 1) | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Option[Int]) => if ($this.content().contains(e)) { | ||
+ | res.isDefined() && $this.size() > res.get() && $this.apply(res.get()) == e | ||
+ | } else { | ||
+ | res.isEmpty() | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List9.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | 1 + t.size() | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$size[T]($this : List0[T]): Int = { | ||
+ | $this match { | ||
+ | case Nil0() => | ||
+ | 0 | ||
+ | case Cons0(h, t) => | ||
+ | 1 + t.size() | ||
+ | } | ||
+ | } ensuring { | ||
+ | (x$1 : Int) => ($this, x$1) passes { | ||
+ | case Cons0(_, Nil0()) => | ||
+ | 1 | ||
+ | case Nil0() => | ||
+ | 0 | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List10.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | h + sum(t) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def sum(l : List0[Int]): Int = { | ||
+ | l match { | ||
+ | case Nil0() => | ||
+ | 0 | ||
+ | case Cons0(h, t) => | ||
+ | h + sum(t) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (x$2 : Int) => (l, x$2) passes { | ||
+ | case Cons0(a, Nil0()) => | ||
+ | a | ||
+ | case Cons0(a, Cons0(b, Nil0())) => | ||
+ | a + b | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% List11.scala %% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | t - e | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$$minus[T]($this : List0[T], e : T): List0[T] = { | ||
+ | $this match { | ||
+ | case Cons0(h, t) => | ||
+ | if (e == h) { | ||
+ | t - e | ||
+ | } else { | ||
+ | Cons0[T](h, t - e) | ||
+ | } | ||
+ | case Nil0() => | ||
+ | Nil0[T]() | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List0[T]) => res.content() == $this.content() -- Set[T](e) | ||
+ | } | ||
+ | |||
+ | %%% List12.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | val scrut = ($this, i); | ||
+ | scrut match { | ||
+ | case (Nil0(), _) => | ||
+ | Nil0[T]() | ||
+ | case (Cons0(h, t), 0) => | ||
+ | scrut._1 | ||
+ | case (Cons0(_, t), i) => | ||
+ | t.drop(2) | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def List0$drop[T]($this : List0[T], i : Int): List0[T] = { | ||
+ | val scrut = ($this, i); | ||
+ | scrut match { | ||
+ | case (Nil0(), _) => | ||
+ | Nil0[T]() | ||
+ | case (Cons0(h, t), 0) => | ||
+ | scrut._1 | ||
+ | case (Cons0(_, t), i) => | ||
+ | t.drop(2) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List0[T]) => (($this, i), res) passes { | ||
+ | case (Cons0(_, Nil0()), 42) => | ||
+ | Nil0[T]() | ||
+ | case (l @ Cons0(_, _), 0) => | ||
+ | l | ||
+ | case (Cons0(a, Cons0(b, Nil0())), 1) => | ||
+ | Cons0[T](b, Nil0[T]()) | ||
+ | case (Cons0(a, Cons0(b, Cons0(c, Nil0()))), 2) => | ||
+ | Cons0[T](c, Nil0[T]()) | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% Numerical1.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | power(base, p - 1) * base | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def power(base : Int, p : Int): Int = { | ||
+ | require(p >= 0) | ||
+ | if (p == 0) { | ||
+ | 1 | ||
+ | } else { | ||
+ | if (p % 2 == 0) { | ||
+ | power(base * base, p / 2) | ||
+ | } else { | ||
+ | power(base, p - 1) * base | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : Int) => ((base, p), res) passes { | ||
+ | case (_, 0) => | ||
+ | 1 | ||
+ | case (b, 1) => | ||
+ | b | ||
+ | case (2, 7) => | ||
+ | 128 | ||
+ | case (2, 10) => | ||
+ | 1024 | ||
+ | } | ||
+ | } | ||
+ | |||
+ | %%% Numerical2.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | (a, 0) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def moddiv(a : Int, b : Int): (Int, Int) = { | ||
+ | require(a >= 0 && b > 0) | ||
+ | if (b > a) { | ||
+ | (a, 0) | ||
+ | } else { | ||
+ | {val x$1 = { | ||
+ | moddiv(a - b, b) match { | ||
+ | case (r1, r2) => | ||
+ | (r1, r2) | ||
+ | } | ||
+ | } | ||
+ | val r1 = { | ||
+ | x$1._1 | ||
+ | } | ||
+ | val r2 = x$1._2; | ||
+ | (r1, (r2 + 1))} | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : (Int, Int)) => b * res._2 + res._1 == a | ||
+ | } | ||
+ | |||
+ | %%% MergeSort1.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | (Cons(b, rec1), Cons(a, rec2)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def split(l : List): (List, List) = { | ||
+ | l match { | ||
+ | case Cons(a, Cons(b, t)) => | ||
+ | val x$1 = { | ||
+ | split(t) match { | ||
+ | case (rec1, rec2) => | ||
+ | (rec1, rec2) | ||
+ | } | ||
+ | } | ||
+ | val rec1 = { | ||
+ | x$1._1 | ||
+ | } | ||
+ | val rec2 = x$1._2; | ||
+ | (Cons(b, rec1), Cons(a, rec2)) | ||
+ | case other => | ||
+ | (other, Nil()) | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : (List, List)) => val x$2 = { | ||
+ | res match { | ||
+ | case (l1, l2) => | ||
+ | (l1, l2) | ||
+ | } | ||
+ | } | ||
+ | val l1 = { | ||
+ | x$2._1 | ||
+ | } | ||
+ | val l2 = x$2._2; | ||
+ | l1.size() >= l2.size() && l1.size() <= l2.size() + 1 && l1.size() + l2.size() == l.size() && l1.content() ++ l2.content() == l.content() | ||
+ | } | ||
+ | |||
+ | %%% MergeSort2.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | Cons[Int](h2, merge(l1, t2)) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(l1 : List[Int], l2 : List[Int]): List[Int] = { | ||
+ | require(isSorted(l1) && isSorted(l2)) | ||
+ | (l1, l2) match { | ||
+ | case (Cons(h1, t1), Cons(h2, t2)) => | ||
+ | if (h1 <= h2) { | ||
+ | Cons[Int](h1, merge(t1, l2)) | ||
+ | } else { | ||
+ | Cons[Int](h2, merge(l1, t2)) | ||
+ | } | ||
+ | case (Nil(), _) => | ||
+ | l2 | ||
+ | case (_, Nil()) => | ||
+ | l1 | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content() | ||
+ | } | ||
+ | |||
+ | %%% MergeSort3.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | h2 >= h1 | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(l1 : List[Int], l2 : List[Int]): List[Int] = { | ||
+ | require(isSorted(l1) && isSorted(l2)) | ||
+ | (l1, l2) match { | ||
+ | case (Cons(h1, t1), Cons(h2, t2)) => | ||
+ | if (h2 >= h1) { | ||
+ | Cons[Int](h1, merge(t1, l2)) | ||
+ | } else { | ||
+ | Cons[Int](h2, merge(l1, t2)) | ||
+ | } | ||
+ | case (Nil(), _) => | ||
+ | l2 | ||
+ | case (_, Nil()) => | ||
+ | l1 | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content() | ||
+ | } | ||
+ | |||
+ | %%% MergeSort4.scala %%% | ||
+ | Found trusted solution! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | h2 :: merge(l1, t2) | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(l1 : List[Int], l2 : List[Int]): List[Int] = { | ||
+ | require(isSorted(l1) && isSorted(l2)) | ||
+ | (l1, l2) match { | ||
+ | case (Cons(h1, t1), Cons(h2, t2)) => | ||
+ | if (h1 <= h2) { | ||
+ | Cons[Int](h1, merge(t1, l2)) | ||
+ | } else { | ||
+ | h2 :: merge(l1, t2) | ||
+ | } | ||
+ | case (Nil(), _) => | ||
+ | l2 | ||
+ | case (_, Nil()) => | ||
+ | l1 | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content() | ||
+ | } | ||
+ | |||
+ | %%% MergeSort5.scala %%% | ||
+ | Solution is not trusted! | ||
+ | ============================== Repair successful: ============================== | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | (l1, l2) match { | ||
+ | case (Nil(), _) => | ||
+ | l2 | ||
+ | case (_, Nil()) => | ||
+ | l1 | ||
+ | case (Cons(h1, t1), Cons(h2, t2)) => | ||
+ | if (h1 <= h2) { | ||
+ | Cons[Int](h1, merge(t1, l2)) | ||
+ | } else { | ||
+ | Cons[Int](h2, merge(l1, t2)) | ||
+ | } | ||
+ | } | ||
+ | ================================= In context: ================================= | ||
+ | --------------------------------- Solution 1: --------------------------------- | ||
+ | def merge(l1 : List[Int], l2 : List[Int]): List[Int] = { | ||
+ | require(isSorted(l1) && isSorted(l2)) | ||
+ | (l1, l2) match { | ||
+ | case (Nil(), _) => | ||
+ | l2 | ||
+ | case (_, Nil()) => | ||
+ | l1 | ||
+ | case (Cons(h1, t1), Cons(h2, t2)) => | ||
+ | if (h1 <= h2) { | ||
+ | Cons[Int](h1, merge(t1, l2)) | ||
+ | } else { | ||
+ | Cons[Int](h2, merge(l1, t2)) | ||
+ | } | ||
+ | } | ||
+ | } ensuring { | ||
+ | (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content() | ||
+ | } | ||
- | The version of Leon used to run all these benchmarks is [[https://github.com/colder/leon/commit/d5a9f51a18100ae762f1d3ef5115e5e8231134bc| publicly available on Github]]. |