From ecd17777499ce89cf133268c4c860bff8272f4e6 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Mon, 27 Apr 2015 19:44:10 -0700
Subject: [PATCH] doc: tutorial now essentially complete. Fixed also the file.
---
doc/tutorial.rst | 96 ++++++++++++++++++++++-----
testcases/web/demos/00_Tutorial.scala | 11 +++
2 files changed, 90 insertions(+), 17 deletions(-)
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index 55f93f1f5..7a5628831 100644
--- a/doc/tutorial.rst
+++ b/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.
diff --git a/testcases/web/demos/00_Tutorial.scala b/testcases/web/demos/00_Tutorial.scala
index dc8734368..786fe3111 100644
--- a/testcases/web/demos/00_Tutorial.scala
+++ b/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)}
+ */
+
}
--
GitLab