diff --git a/doc/intro.rst b/doc/intro.rst index d1d4e8b5fd1362256b510774b48cc123d8c6df32..f25e9a3a47166234cd5812b50e0f863b2c2977f4 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 1a881b7ed6ab7f73fc59073b4c7528371fd9e3ce..609c5bb454ad068e1a0a7c652976d1a9f6e806ee 100644 --- a/doc/repair.rst +++ b/doc/repair.rst @@ -1,2 +1,4 @@ +.. _repair: + Repair ======