From 4d62a4229f5c289ff527cac760d0e31199932028 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 23 Apr 2015 18:48:40 +0200
Subject: [PATCH] Repair intro
---
doc/intro.rst | 49 ++++++++++++++++++++++++++++++++++++++++++++++++-
doc/repair.rst | 2 ++
2 files changed, 50 insertions(+), 1 deletion(-)
diff --git a/doc/intro.rst b/doc/intro.rst
index d1d4e8b5f..f25e9a3a4 100644
--- a/doc/intro.rst
+++ b/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>`.
+
diff --git a/doc/repair.rst b/doc/repair.rst
index 1a881b7ed..609c5bb45 100644
--- a/doc/repair.rst
+++ b/doc/repair.rst
@@ -1,2 +1,4 @@
+.. _repair:
+
Repair
======
--
GitLab