From 45046b42258788d2f56a7e4c14753e7b8f116c96 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 27 Mar 2015 16:22:11 +0100
Subject: [PATCH] a more evolved intro
---
doc/index.rst | 2 +-
doc/intro.rst | 45 +++++++++++++++++++++++++++++++++++++++++++--
2 files changed, 44 insertions(+), 3 deletions(-)
diff --git a/doc/index.rst b/doc/index.rst
index bb9f64509..0c972a995 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -12,8 +12,8 @@ Contents:
:maxdepth: 2
intro
- installation
gettingstarted
+ installation
purescala
xlang
verification
diff --git a/doc/intro.rst b/doc/intro.rst
index 389973660..7f6caa980 100644
--- a/doc/intro.rst
+++ b/doc/intro.rst
@@ -1,8 +1,49 @@
Introduction
============
-The Leon system is an automated system for verifying, repairing, and synthesizing functional Scala programs.
+The Leon system is an automated system for verifying, repairing, and
+synthesizing Scala programs.
-Leon supports programs written in :ref:`purescala`, a purely functional subset of Scala.
+Leon supports programs written in :ref:`Pure Scala <purescala>`, a purely
+functional subset of Scala. The :ref:`XLang <xlang>` extension enables Leon to
+work on a richer subset of Scala, including imperative features. From the
+perspective of the end user, that distinction between the two sets of features
+should be mostly meaningless, but it can help getting an intuition when trying
+to prove difficult properties.
+The :ref:`Pure Scala <purescala>` features are at the *core* of the Leon
+system. They are considered as primitives and get a personalized treatment in
+the solving algorithms of Leon. On the other hand, any feature introduced by
+:ref:`XLang <xlang>` can be --- and is --- encoded into a mix of Pure Scala
+concepts. However, they are more than just syntactic sugar --- some of those
+features actually require significant modification of the original program.
+Software Verification
+---------------------
+
+Leon started out as a program verifier for :ref:`Pure Scala <purescala>`. It
+would collect a list of top level functions written in Pure Scala, and verifies
+the *validity* of their *contracts*. Essentially, for each function,
+it would prove that the postcondition always hold, assuming a given precondition does
+hold. A simple example:
+
+.. code-block:: scala
+ def factorial(n: Int): Int = {
+ require(n >= 0)
+ if(n == 0) 1 else n * factorial(n - 1)
+ } ensuring(res => res >= 0)
+
+Leon generates a ``postcondition`` verification condition for the above
+function, corresponding to the predicate parameter to the ``ensuring``
+expression. It attempts to prove it using a combination of an internal
+algorithm and external automated theorem proving. Leon will return one of the
+following:
+
+* The postcondition is `valid`. In that case, Leon was able to prove that for **any**
+ input to the function satisfiying the precondition, the postcondition will always hold.
+* The postcondition is `invalid`. It means that Leon disproved the postcondition and
+ that there exists at least one input satisfying the precondition and such that the
+ postcondition does not hold. Leon will always return a concrete counterexample, very
+ useful when trying to understand why a function is not satisfying its contract.
+* The postcondition is `unknown`. It means Leon is unable to prove or find a counterexample.
+ It usually happens after a timeout or an internal error in the external theorem prover.
--
GitLab