Repair intro

doc/intro.rst

@@ -68,4 +68,51 @@ Program Synthesis
 
 
 Program Repair
---------------
+-------------
+
+Leon can repair buggy :ref:`Pure Scala <purescala>` programs.
+Given a specification and an erroneous implementation, Leon will
+localize the cause of the bug and provide an alternative solution.
+An example:
+
+.. code-block:: scala
+
+   def moddiv(a: Int, b: Int): (Int, Int) = {
+     require(a >= 0 && b > 0);
+     if (b > a) {
+       (1, 0) // fixme: should be (a, 0)
+     } else {
+       val (r1, r2) = moddiv(a-b, b)
+       (r1, r2+1)
+     }
+   } ensuring {
+     res =>  b*res._2 + res._1 == a
+   }
+
+Invoking ``leon --repair --functions=moddiv`` will yield: ::
+
+  ...
+  [  Info  ] Found trusted solution!
+  [  Info  ] ============================== Repair successful: ==============================
+  [  Info  ] --------------------------------- Solution 1: ---------------------------------
+  [  Info  ] (a, 0)
+  [  Info  ] ================================= In context: =================================
+  [  Info  ] --------------------------------- Solution 1: ---------------------------------
+  [  Info  ] def moddiv(a : Int, b : Int): (Int, Int) = {
+               require(a >= 0 && b > 0)
+               if (b > a) {
+                 (a, 0)
+               } else {
+                 val (r1, r2) = moddiv(a - b, b)
+                 (r1, (r2 + 1))
+               }
+             } ensuring {
+               (res : (Int, Int)) => (b * res._2 + res._1 == a)
+             }
+
+Repair assumes a small number of localized errors.
+It first invokes a test-based fault localization algorithm,
+and then a special synthesis procedure, which is partially guided
+by the original erroneous implementation. For more information,
+see the section on :ref:`Repair <repair>`.
+

doc/repair.rst

+.. _repair:
+
 Repair
 ======