From f9e2fb533a2e1d885382f4dd56c49dceab6c3527 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Tue, 28 Apr 2015 11:34:48 -0700
Subject: [PATCH] doc: more in tutorial

---
 doc/tutorial.rst | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index 7a5628831..e9980917e 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -432,7 +432,23 @@ As the starting point, we define size of a list.
         case Cons(x, rest) => 1 + size(rest)
     })
 
-We can add a specification that the size is non-negative.
+The definition uses *pattern matching* to define size of the
+list in the case it is empty (where it is zero) and when it
+is non-empty, or, if its non-empty, then it has a head `x`
+and the rest of the list `rest`, so the size is one plus the
+size of the rest. Thus `size` is a recursive function.  A
+strength of Leon is that it allows using such recursive
+functions in specifications.
+
+It makes little sense to try to write a complete
+specification of `size`, given that its recursive definition
+is already a pretty clear description of its
+meaning. However, it is useful to add a consequence of this
+definition, namely that the size is non-negative. The reason
+is that Leon most of the time reasons by unfolding `size`,
+and the property of size being non-negative is not revealed
+by such unfolding. Once specified, the non-negativity is
+easily proven and Leon will make use of it.
 
 .. code-block:: scala
 
@@ -479,7 +495,9 @@ which is a building block for an insertion sort.
 
 Leon verifies that the returned list is indeed sorted. Note
 how we are again using a recursively defined function to
-specify another function.
+specify another function. We can introduce a bug into the
+definition above and examine the counterexamples that Leon
+finds.
 
 Being Sorted is Not Enough
 --------------------------
-- 
GitLab