Describe the rest of XLang

doc/xlang.rst

@@ -3,17 +3,17 @@
 XLang
 =====
 
-To complement the core PureScala language, the XLang module of Leon brings a
-few extensions to that core language.
+To complement the core :ref:`Pure Scala <purescala>` language, the XLang module
+of Leon brings a few extensions to that core language.
 
 These extensions are kept as an optional feature, that needs to be explicitly
 enabled from the command line with the option ``--xlang``. If you do not specify
 the option, Leon will reject any program making use of an XLang feature.
 
-Technically, these extensions are implemented using a translation to PureScala.
-This means They are not implemented in the back-end solving system of Leon, but
-parsed in the the front-end and eliminate early during the Leon pipelining
-process.
+Technically, these extensions are implemented using a translation to :ref:`Pure
+Scala <purescala>`. This means They are not implemented in the back-end
+solving system of Leon, but parsed in the the front-end and eliminate early
+during the Leon pipelining process.
 
 Imperative Code
 ---------------
@@ -42,9 +42,9 @@ The above example illustrates three new features introduced by XLang:
 You can use Scala variables with a few restrictions. The variables can only be
 declared and used locally in the same function, and inner functions cannot
 close over them. XLang introduces the possibility to use sequences of
-expressions (blocks) -- a feature not available in PureScala, where you're only
-option is a sequence of ``val`` which essentially introduce nested ``let``
-declarations.
+expressions (blocks) -- a feature not available in :ref:`Pure Scala
+<purescala>`, where you're only option is a sequence of ``val`` which
+essentially introduce nested ``let`` declarations.
 
 .. warning::
    Be careful when combining variables with nested functions from PureScala. Leon
@@ -93,19 +93,92 @@ as ``valid``.
 
 Leon internally handle loops as a function with a postcondition. For the end-user it
 means that Leon is only going to rely on the postcondition of the loop to prove properties
-of code relying on loops.
+of code relying on loops. Usually that invariant is too weak to prove anything remotely
+useful and you will need to anotate the loop with a stronger invariant.
+
+You can anotate a loop with an invariant as follows:
+
+.. code-block:: scala
+
+   var res = 0
+   var i = 0
+   (while(i < 10) {
+     res = res + i
+     i = i + 1
+   }) invariant(i >= 0 && res >= i)
+
+The strange syntax comes from some Scala magic in order to make the keyword
+``invariant`` a valid keyword. Leon is defining an implicit conversion from
+``Unit`` to an ``InvariantFunction`` object that provides an ``invariant``
+method. The ``invariant`` method takes a boolean expression as a parameter and
+its semantics is to hold at the following points during the execution of the loop:
+
+1. When first entering the loop: initialization.
+2. After each complete execution of the body.
+3. On exiting the loop.
+
+Leon will generate verification conditions ``invariant inductive`` and
+``invariant postcondition`` to verify points (2) and (3) above. It will also
+generate a ``precondition`` corresponding to the line of the while loop. This
+verification condition is used to prove the invariant on initialization of the
+loop.
 
 Arrays
 ******
 
-PureScala supports functional arrays, that is, the operations ``apply`` and ``updated`` which do
-not modify an array but only returns some result. In particular, ``updated`` returns a new copy
-of the array.
+PureScala supports functional arrays, that is, the operations ``apply`` and
+``updated`` which do not modify an array but only returns some result. In
+particular, ``updated`` returns a new copy of the array.
+
+.. code-block:: scala
+
+   def f(a: Array[Int]): Array[Int] = {
+     a(0).updated(0, a(1))
+   }
+
+However, using functional arrays is not the most natural way to work with
+arrays, and arrays are often used in imperative implementations of algorithms.
+XLang adds the usual ``update`` operation on arrays:
+
+.. code-block:: scala
 
-.. note::
-   some note comes here
+   val a = Array(1,2,3,4)
+   a(1) //2
+   a(1) = 10
+   a(1) //10
+
+There are some limitations with what you can do with arrays. Leon simply
+rewrite arrays using ``update`` operation as assignment of function arrays
+using ``updated``.  This leverages the built-in algorithm for functional array
+and rely on the elimination procedure for assignments. Concretely, it would
+transform the above on the following equivalent implementation:
+
+.. code-block:: scala
+
+   var a = Array(1,2,3,4)
+   a(1) //2
+   a = a.updated(1, 10)
+   a(1) //10
+
+Then Leon would apply the same process as for any other XLang program.
+
+Due to the way Leon handles side-effects, you cannot update arrays passed
+to a function as a parameter.
 
 Epsilon
 -------
 
+XLang introduces the ``epsilon`` keyword to express non-determinism. The
+concept is inspired from `Hilbert's epsilon calculus
+<http://en.wikipedia.org/wiki/Epsilon_calculus>`_. An ``epsilon`` expression
+takes a predicate as parameter and is defined to return a value that
+satisfies the predicate:
+
+.. code-block:: scala
+
+   def getInRange(from: Int, to: Int): Int = {
+     epsilon(n => from <= n && n <= to)
+   }
 
+You can use epsilon when you only know the interface of some function but
+cannot provide a concrete implementation.