From 736e690a8f4aa74b047a2780dde067f5d9c78d4e Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 23 Mar 2015 11:42:34 +0100
Subject: [PATCH] Describe the rest of XLang
---
doc/xlang.rst | 103 ++++++++++++++++++++++++++++++++++++++++++--------
1 file changed, 88 insertions(+), 15 deletions(-)
diff --git a/doc/xlang.rst b/doc/xlang.rst
index 5089d8b93..e58675563 100644
--- a/doc/xlang.rst
+++ b/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.
--
GitLab