doc: tutorial now essentially complete. Fixed also the file.

doc/tutorial.rst

@@ -12,6 +12,7 @@ This tutorial shows how to:
   * use sets and recursive function to specify data structures
   * synthesize insertion into a sorted list
   * synthesize sorting on lists
+  * repair an incorrect function
 
 We assume that the user is using the web interface. The
 functionality is also available (possibly with less
@@ -461,6 +462,9 @@ order.
 Insertion into Sorted List
 --------------------------
 
+Consider the following specification of insertion into a sorted list,
+which is a building block for an insertion sort.
+
 .. code-block:: scala
 
   def sInsert(x : BigInt, l : List) : List = {
@@ -473,10 +477,14 @@ Insertion into Sorted List
     }
   } ensuring {(res:List) => isSorted(res)}
 
+Leon verifies that the returned list is indeed sorted. Note
+how we are again using a recursively defined function to
+specify another function.
+
 Being Sorted is Not Enough
 --------------------------
 
-A function such as this one is correct.
+Note, however, that a function such as this one is also correct.
 
 .. code-block:: scala
 
@@ -485,7 +493,8 @@ A function such as this one is correct.
       Nil
     } ensuring {(res:List) => isSorted(res)}
 
-So, our specification may be considered weak.
+So, our specification may be considered weak, because it does
+not say anything about the elements.
 
 Using Size in Specification
 ---------------------------
@@ -498,7 +507,7 @@ Consider a stronger additional postcondition property:
 
 Does it hold? If we try to add it, we obtain a counterexample.
 A correct strengthening, taking into account that the element
-may or may not already be in the list, is:
+may or may not already be in the list, is the following.
 
 .. code-block:: scala
 
@@ -523,8 +532,9 @@ of the list.
   } ensuring {(res:List) => 
      isSorted(res) && content(res) == content(l) ++ Set(x)}
 
-To compute content, in this example we use sets, even though
-it might be better in general to use multisets.
+To compute `content`, in this example we use sets (even
+though in general it might be better in general to use bags
+i.e. multisets).
 
 .. code-block:: scala
 
@@ -537,25 +547,28 @@ it might be better in general to use multisets.
 Sorting Specification and Running It
 ------------------------------------
 
+Specifying sorting is in fact very easy.
+
 .. code-block:: scala
 
-  def sortMagic(l : List) = choose{(res:List) => 
-    isSorted(res) && content(res) == content(l)
-  }
+  def sortMagic(l : List) = {
+     ???[List]
+  } ensuring((res:List) => 
+    isSorted(res) && content(res) == content(l))
 
-We can execute it.
+We can execute such a sort.
 
 .. code-block:: scala
 
   def mm = sortMagic(Cons(20, Cons(5, Cons(50, Cons(2, Nil)))))
 
 obtaining the expected `Cons(2, Cons(5, Cons(20, Cons(50, Nil))))`.
-
+Note that the function actually removes duplicates from the input list.
 
 Synthesizing Sort
 -----------------
 
-By asking the system to synthesize the `choose` construct,
+By asking the system to synthesize the `choose` construct inside `magicSort`,
 we may obtain a function such as the following, which gives
 us the natural insertion sort.
 
@@ -572,15 +585,64 @@ us the natural insertion sort.
 Going back and Synthesizing Insertion
 -------------------------------------
 
-In fact, if we had a precise enough specification of insert,
-we could have synthesized it from the specification.
+In fact, if we have a reasonably precise enough
+specification of insert, we can synthesize the implementation.
+To try this, remove the body of `sInsert` and replace it
+with `???[List]` denoting an unknown value of the given type.
+
+.. code-block:: scala
+
+  def sInsert(x : BigInt, l : List) : List = {
+    require(isSorted(l))
+    ???[List]
+  } ensuring {(res:List) => 
+     isSorted(res) && content(res) == content(l) ++ Set(x)}
+
+Leon can then synthesize the missing part, resulting in a similar
+body to the one we wrote by hand originally.
+
+Repairing an Incorrect Function
+-------------------------------
+
+You may notice that synthesis can take a long time and fail.
+Often we do produce some version of the program, but it is
+not correct according to a specification.  Consider the
+following attempt at `sInsert`.
 
 .. code-block:: scala
 
-  def insertMagic(x: BigInt, l: List): List = {
+  def sInsert(x : BigInt, l : List) : List = {
     require(isSorted(l))
-    choose {(res: List) => 
-      isSorted(res) && content(res) == content(l) ++ Set[BigInt](x)
+    l match {
+      case Nil => Cons(x, Nil)
+      case Cons(e, rest) => Cons(e, sInsert(x,rest))
     }
-  }
+  } ensuring {(res:List) => 
+     isSorted(res) && content(res) == content(l) ++ Set(x)}
+
+Leon reports a counterexample to the correctness. Instead of
+trying to manually understand the counterexample, we can
+instruct the system to **repair** this solution. If Leon can
+reuse parts of the existing function, it can be much faster
+than doing synthesis from scratch. Leon automatically finds
+test inputs that it uses to localize the error and preserve
+useful existing pieces of code. In this case, Leon repairs
+the above function into the one equivalent to the original
+one, by doing a case split and synthesizing two new cases,
+resulting in the following equivalent function.
+
+.. code-block:: scala
+
+  def sInsert(x : BigInt, l : List): List = {
+    require(isSorted(l))
+    l match {
+    case Nil => Cons(x, Nil)
+    case Cons(e, rest) =>
+      if (x < e) Cons(x, l)
+      else if (x == e) Cons(x, rest)
+      else Cons(e, sInsert(x, rest))
+  } ensuring { (res : List) => 
+    isSorted(res) && content(res) == content(l) ++ Set[BigInt](x) }
+
 
+This completes the tutorial. To learn more, check the rest of this documentation and browse the examples provided with Leon.

testcases/web/demos/00_Tutorial.scala

@@ -174,4 +174,15 @@ def max(x: Int, y: Int): Int = {
 
   // def mm = sortMagic(Cons(20, Cons(5, Cons(50, Cons(2, Nil)))))
 
+/*
+  def sInsert(x : BigInt, l : List) : List = {
+    require(isSorted(l))
+    l match {
+      case Nil => Cons(x, Nil)
+      case Cons(e, rest) => Cons(e, sInsert(x,rest))
+    }
+  } ensuring {(res:List) => 
+     isSorted(res) && content(res) == content(l) ++ Set(x)}
+ */
+
 }