Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
leon-repair [2015/02/09 14:58]
ekneuss
leon-repair [2015/02/10 17:14] (current)
ekneuss
Line 47: Line 47:
  
 The version of Leon used to run all these benchmarks is [[https://​github.com/​colder/​leon/​tree/​ddd08e3aac4cc52c51dc60b59867eaea38f3cbf5| publicly available on Github]]. 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()
 + }
  
 
leon-repair.txt · Last modified: 2015/02/10 17:14 by ekneuss
 
© EPFL 2018 - Legal notice