diff --git a/doc/repair.rst b/doc/repair.rst
index 609c5bb454ad068e1a0a7c652976d1a9f6e806ee..dc6103a5547e4cc5f1dfb7c13945b5a27b2e3677 100644
--- a/doc/repair.rst
+++ b/doc/repair.rst
@@ -2,3 +2,209 @@
Repair
======
+
+Leon can repair buggy :ref:`Pure Scala <purescala>` programs.
+Given a specification and an erroneous implementation for a function,
+Leon will localize the cause of the bug and provide an alternative solution.
+In the following we will give some insight into how repair works
+through a simple example.
+
+An example
+-----------
+
+In the following code, a user has tried to implement a function
+that performs natural number division using only addition and subtraction.
+However, this snippet contains a bug:
+
+.. 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
+ }
+
+Leon can discover and repair this error.
+Invoking ``leon --repair --functions=moddiv`` will yield: ::
+
+ [ Info ] ======================= 1. Discovering tests for moddiv =======================
+ [ Info ] - Passing: 1
+ [ Info ] - Failing: 5
+ [ Info ] - Minimal Failing Set Size: 2
+ [ Info ] Finished in 836ms
+ [ Info ] ==================== 2. Locating/Focusing synthesis problem ====================
+ [ Info ] Program size : 152
+ [ Info ] Original body size: 30
+ [ Info ] Focused expr size : 3
+ [ Info ] Finished in 78ms
+ [ Info ] =============================== 3. Synthesizing ===============================
+ [ Info ] ⟦ a;b, ↓ moddiv(a, b) && ⊙ {(1, 0)} && a >= 0 && b > 0 && b > a ≺ ⟨ val res = x27;
+ [ Info ] b * res._2 + res._1 == a ⟩ x27 ⟧
+ [ Info ] [CEGLESS ] ⟦ a;b, ↓ moddiv(a, b) && ⊙ {(1, 0)} && a >= 0 && b > 0 && b > a ≺ ⟨ val res = x27;
+ [ Info ] b * res._2 + res._1 == a ⟩ x27 ⟧
+ [ Info ] [CEGLESS ] Solved with: ⟨ true | (a, 0) ⟩...
+ [ Info ] Finished in 1995ms
+ [ 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)
+ }
+
+Leon has localized the error on the expression ``(1, 0)`` and provided
+the correct alternative ``(a, 0)``, as well as the entire repaired function
+(due to some implementation restrictions,
+the function body which Leon outputs is a little more complex than
+the one given above, but equivalent to it).
+
+Repair Mechanism
+----------------
+
+We can break down the repair mechanism of Leon in three phases:
+
+Test Case Generation
+********************
+
+In the beginning, Leon will try to generate test cases which will
+help localize the error. Sample inputs are generated by an enumeration
+technique, and then the function under repair is executed on them.
+The test cases are divided in passing (those that satisfy the function
+specification) and failing. What we are actually interested in are
+the failing test cases; if none are generated, we resort to an SMT
+solver to discover a counterexample for the function (or possibly
+prove it correct).
+
+Next, a dependency analysis is run on the discovered failing tests,
+and those that recursively invoke the function with another failing input
+are rejected.
+
+Fault Localization
+******************
+
+In the next step, Leon will try to localize the problem to the smallest
+possible subexression of the function body. The idea is to run the failing
+test cases through the function and isolate the paths followed by some erroneous
+executions. In ``moddiv``, Leon will successfully identify the expression ``(1, 0)``
+as the source of the error. Repair will work even in the presence of more than one
+errors; however, the discovered subexpression may be larger. This is compensated
+for in a later stage.
+
+Because of this approach, repair works better for programs
+that contain a small number of localized errors.
+Errors that wrap the whole body of the function will fail to be localized,
+and repair will fall back to generic synthesis.
+
+Synthesis of the Repaired Expression
+************************************
+
+Leon then tries to synthesize an alternative expression in place of the
+erroneous one which satisfies the function specification. To this, it uses
+generic :ref:`synthesis`, enhanced with a rule for similar term exploration,
+due to our hypothesis of small localized errors.
+
+Verification of the synthesized solution
+****************************************
+
+Finally, Leon will try to verify the synthesized solution. In case of
+failure to prove it correct (but also to disprove it), Leon will still
+present it as an untrusted solution.
+
+Repairing with IO-examples
+--------------------------
+
+Sometimes, a complete formal specification is hard to express,
+especially when it comes to simple, elementary functions. In such cases,
+it may be easier to provide a set of IO-examples. However, IO-examples can never
+cover all the possible executions of the function and are thus weaker than a formal
+specification.
+
+Leon provides a powerful compromise between these two extremes.
+It introduces *symbolic IO-examples*, expressed through a specialized ``passes``
+construct, which resembles pattern-matching:
+
+.. code-block:: scala
+
+ sealed abstract class List {
+ def drop(i: Int): List[T] = { (this, i) match {
+ case (Nil(), _) => Nil()
+ case (Cons(h, t), ) =>
+ t // FIXME should be this
+ case (Cons(_, t), i) =>
+ t.drop(i) //FIXME should be i-1
+ }} ensuring { res => ((this, i), res) passes {
+ case (Cons(_, Nil()), 42) => Nil()
+ case (l@Cons(_, _), 0) => l
+ case (Cons(a, Cons(b, Nil())), 1) => Cons(b, Nil())
+ case (Cons(a, Cons(b, Cons(c, Nil()))), 2) => Cons(c, Nil())
+ }}
+ }
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+
+In the above example, the programmer has chosen to specify drop through a
+list of IO-examples, describing what the function should do in the cases where
+the elements to drop are more than the size of the list,
+or 0, 1 or 2 elements are to be dropped by a list with enough elements.
+Notice that the examples are symbolic, in that the elements of the lists are
+left as arbitrary values.
+
+The semantics of ``passes: ( (A, B) => Boolean)`` are the following:
+
+.. code-block:: scala
+
+ (a, b) passes {
+ case p1 => e1
+ case p2 => e2
+ ...
+ case pN => eN
+ }
+
+where ``a: A`` is a tuple of method parameters and/or ``this``, ``b: B``,
+and for each i ``pi: A`` and ``ei: B``, is equivalent to
+
+.. code-block:: scala
+
+ a match {
+ case p1 => b == e1
+ case p2 => b == e2
+ ...
+ case pN => b == eN
+ case _ => true
+ }
+
+Leon will manage to repair this program: ::
+
+ ...
+ [ Info ] Found trusted solution!
+ [ Info ] ============================== Repair successful: ==============================
+ [ Info ] --------------------------------- Solution 1: ---------------------------------
+ [ Info ] val scrut = ($this, i);
+ [ Info ] scrut match {
+ [ Info ] case (Nil(), _) =>
+ [ Info ] Nil[T]()
+ [ Info ] case (Cons(h, t), 0) =>
+ [ Info ] scrut._1
+ [ Info ] case (Cons(_, t), i) =>
+ [ Info ] t.drop(i - 1)
+ [ Info ] }
+ ...
+
+
diff --git a/doc/synthesis.rst b/doc/synthesis.rst
index 8b283bcd2d42147677503a7a4d07513e1f50749f..46dcaa860444750a7f295e7ab577a45f3a427a54 100644
--- a/doc/synthesis.rst
+++ b/doc/synthesis.rst
@@ -1,2 +1,4 @@
+.. _synthesis:
+
Synthesis
=========