diff --git a/src/sphinx/index.rst b/src/sphinx/index.rst
index 0dc9d673eb7ce2d812675dcec6294d6ab227c8ad..c80f95d406be4a03276d8994b5b3334d5cde8b4c 100644
--- a/src/sphinx/index.rst
+++ b/src/sphinx/index.rst
@@ -19,6 +19,7 @@ Contents:
library
xlang
verification
+ isabelle
neon
limitations
synthesis
diff --git a/src/sphinx/installation.rst b/src/sphinx/installation.rst
index 49251612de00d0cfc97f1e961da37db2378280c0..f8de2929d040cf45dfe068eecba15a208d4ae61e 100644
--- a/src/sphinx/installation.rst
+++ b/src/sphinx/installation.rst
@@ -13,9 +13,9 @@ Windows.
**Requirements:**
-* `1.7 Java Development Kit <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_
+* `Java SE Development Kit 7 <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_
-* SBT 0.13.X (Available from http://www.scala-sbt.org/)
+* SBT 0.13.x (Available from http://www.scala-sbt.org/)
* Support for at least one SMT solver (See :ref:`smt-solvers`)
@@ -45,7 +45,8 @@ all the appropriate settings:
Windows
-------
-Get the sources of Leon by cloning the official Leon repository (You will need a git shell for windows e.g. https://msysgit.github.io/):
+Get the sources of Leon by cloning the official Leon repository. You will need
+a Git shell for windows, e.g. `Git for Windows <https://git-for-windows.github.io/>`_.
.. code-block:: bash
@@ -72,8 +73,8 @@ under Cygwin.
If running leon produces errors because it could not find some cafebabe*.jar or vanuatoo*.jar, it is probably because symlinks have not been resolved. If your architecture is x64, do the following:
-1. Copy unmanaged/common/cafebabe*.jar to unmanaged/64/
-2. Copy unmanaged/common/vanuatoo*.jar to unmanaged/64/
+1. Copy ``unmanaged/common/cafebabe*.jar`` to ``unmanaged/64/``
+2. Copy ``unmanaged/common/vanuatoo*.jar`` to ``unmanaged/64/``
.. _smt-solvers:
@@ -98,7 +99,10 @@ their binaries available in the ``$PATH``.
Since the default solver uses the native Z3 API, you will have to explicitly
specify another solver if this native layer is not available to you. Check also
-the ``--solvers`` option in :ref:`cmdlineoptions` .
+the ``--solvers`` option in :ref:`cmdlineoptions`.
+
+Alternatively, there is a non-SMT solver available. See :ref:`isabelle` for
+details.
Building Documentation
----------------------
diff --git a/src/sphinx/isabelle.rst b/src/sphinx/isabelle.rst
new file mode 100644
index 0000000000000000000000000000000000000000..9392b519a2276b8efd08d2098090080a9960fe62
--- /dev/null
+++ b/src/sphinx/isabelle.rst
@@ -0,0 +1,243 @@
+.. _isabelle:
+
+Isabelle
+========
+
+Isabelle is an interactive theorem prover. It comes with an IDE where users can
+type mathematical specifications and proofs which will be checked continuously.
+Specifications consist of a sequence of type and value definitions. All
+high-level tools inside Isabelle must justify their proofs and constructions
+against a small inference kernel. This greatly diminishes the risk of unsound
+proofs.
+
+Additionally, Isabelle features powerful proof automation, for example:
+
+ - classical and equational reasoning
+ - decision procedures (e.g. for linear arithmetic)
+ - interfaces to automated provers (e.g. Z3 and CVC4)
+
+However, most non-trivial proofs will require the user to give proof hints. In
+general, interactive provers like Isabelle trade better guarantees for weaker
+automation.
+
+Normally, users write Isabelle specifications manually. Leon comes with a
+bridge to Isabelle which allows it to be used as a solver for program
+verification.
+
+
+Installation
+------------
+
+You can obtain a copy of Isabelle for your operating system at `its website
+<https://isabelle.in.tum.de/>`_, then follow the `installation instructions
+<https://isabelle.in.tum.de/installation.html>`_. The installation path needs
+to be passed to Leon via the ``--isabelle:base`` command line option. (The path
+will end in ``Isabelle2015``. Depending on your operating system, this folder
+might be some levels into the installation tree.)
+
+On Linux, you can skip this step. Leon is able to download and install Isabelle
+itself. During the first start, you just need to pass the command line option
+``--isabelle:download=true``. You may specify ``--isabelle:base``, but don't
+have to.
+
+
+Basic usage
+-----------
+
+For most purposes, Isabelle behaves like any other solver. When running
+:ref:`verification`, you can pass ``isabelle`` as a solver (see
+:ref:`cmdlineoptions` for details). Isabelle is a bit slower to start up than
+the other solvers, so please be patient.
+
+
+Advanced usage
+--------------
+
+Isabelle has some peculiarities. To accomodate for those, there are a set of
+specific annotations in the object ``leon.annotation.isabelle``.
+
+
+Mapping Leon entities to Isabelle entities
+******************************************
+
+Isabelle -- or it's standard logic *HOL*, to be precise -- ships with a rather
+large existing library. By default, the Isabelle backend would just translate
+all Leon definitions into equivalent Isabelle definitions, which means that
+existing proofs about them are not applicable. For example, Isabelle/HOL already
+has a concatenation function for lists and an associativity proof for it. The
+annotations ``@typ``, ``@constructor`` and ``@function`` allow the user to
+declare a mapping to existing Isabelle entities. For lists and their append
+function, this looks like this:
+
+.. code-block:: scala
+
+ @isabelle.typ(name = "List.list")
+ sealed abstract class List[T] {
+
+ @isabelle.function(term = "List.append")
+ def ++(that: List[T]): List[T] = (this match {
+ case Nil() => that
+ case Cons(x, xs) => Cons(x, xs ++ that)
+ })
+
+ }
+
+ @isabelle.constructor(name = "List.list.Cons")
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+
+ @isabelle.constructor(name = "List.list.Nil")
+ case class Nil[T]() extends List[T]
+
+The above is a simplified excerpt from Leon's standard library. However, it is
+no problem to map functions with postconditions to their Isabelle equivalents.
+
+By default, mapping for types is loosely checked, whereas mapping for functions
+is checked:
+
+ - For types, it is checked that there are exactly as many constructors in Leon
+ as in Isabelle and that all constructors are annotated. It is also checked
+ that the given constructor names actually exist and that they have the same
+ number of arguments, respectively. There is no check whether the field types
+ are equivalent. However, in most cases, such a situation would be caught
+ later because of type errors.
+
+ - For functions, a full equivalence proof is being performed. First, the
+ function will be translated to Isabelle as usual. Second, the system will
+ try to prove that both definitions are equivalent. If that proof fails, the
+ system will emit a warning and ignore the mapping.
+
+The checking behaviour can be influenced with the ``strict`` option (see
+:ref:`cmdlineoptions`).
+
+
+Scripting source files
+**********************
+
+The ``script`` annotation allows to embed arbitrary Isabelle text into Leon
+source files. In the following example, this is used together with mapping:
+
+.. code-block:: scala
+
+ @isabelle.script(
+ name = "Safe_Head",
+ source = """
+ fun safe_head where
+ "safe_head [] = None" |
+ "safe_head (x # _) = Some x"
+
+ lemma safe_head_eq_head[simp]:
+ assumes "~ List.null xs"
+ shows "safe_head xs = Some (hd xs)"
+ using assms
+ by (cases xs) auto
+ """
+ )
+ @isabelle.function(term = "Safe_Head.safe_head")
+ def safeHead[A](xs: List[A]): Option[A] = xs match {
+ case Nil() => None()
+ case Cons(x, _) => Some(x)
+ }
+
+``script`` annotations are processed only for functions which are directly or
+indirectly referenced from the source file which is under verification by Leon.
+The effect of a script is equivalent to defining an Isabelle theory with the
+name and content as specified in the annotation, importing the ``Leon`` theory.
+Theories created via script annotations must be independent of each other, but
+are processed before everything else. As a consequence, any entities defined
+in scripts are available for all declarations.
+
+.. note::
+
+ Invalid proofs will raise an error, but skipped proofs (with ``sorry``) are
+ not reported.
+
+
+Proof hints
+***********
+
+The system uses a combination of tactics to attempt to prove postconditions of
+functions. Should these fail, a custom proof method can be specified with the
+``proof`` annotation.
+
+.. code-block:: scala
+
+ @isabelle.proof(method = """(induct "<var xs>", auto)""")
+ def flatMapAssoc[A, B, C](xs: List[A], f: A => List[B], g: B => List[C]) =
+ (xs.flatMap(f).flatMap(g) == xs.flatMap(x => f(x).flatMap(g))).holds
+
+The method string is interpreted as in Isabelle:
+
+.. code-block:: text
+
+ lemma flatMapAssoc: ...
+ by (induct "<var xs>", auto)
+
+.. note::
+
+ In annotations, the function parameters are not in scope. That means that
+ referring to the actual Scala variable ``xs`` is impossible. Additionally,
+ in Isabelle, ``xs`` will not be called ``xs``, but rather ``xs'76`` (with
+ the number being globally unique). To be able to refer to ``xs``, the system
+ provides the special input syntax ``<var _>``, which turns an identifier
+ of a variable into its corresponding variable in Isabelle. Think of it as a
+ quotation for Scala in Isabelle. There is also a counterpart for constants:
+ ``<const _>``.
+
+The ``proof`` annotations admits a second argument, ``kind``, which specifies a
+comma-seperated list of verification conditions it should apply to. The empty
+string (default) means all verification conditions.
+
+
+Influencing the translation of functions
+****************************************
+
+By default, the system will only translate the body of a function, that is,
+without pre- and postconditions, to Isabelle. Sometimes, the precondition is
+required for termination of the function. Since Isabelle doesn't accept
+function definitions for which it can't prove termination, the presence of the
+precondition is sometimes necessary. This can be achieved by annotating the
+function with ``@isabelle.fullBody``. If, for other reasons, termination can't
+be proven, the annotation ``@isabelle.noBody`` leaves the function unspecified:
+It can still be called from other functions, but no proofs depending on the
+outcome of the functions will succeed.
+
+
+Advanced example
+----------------
+
+The following example illustrates the definition of a tail-recursive function.
+The challenge when proving correctness for these kinds of functions is that
+"simple" induction on the recursive argument is often not sufficient, because
+the other arguments change in the recursive calls. Hence, it is prudent to
+specify a proof hint. In this example, an induction over the definition of the
+``lenTailrec`` function proves the goal:
+
+.. code-block:: scala
+
+ def lenTailrec[T](xs: List[T], n: BigInt): BigInt = xs match {
+ case Nil() => n
+ case Cons(_, xs) => lenTailrec(xs, 1 + n)
+ }
+
+ @isabelle.proof(method = """(induct "<var xs>" "<var n>" rule: [[leon_induct lenTailrec]], auto)""")
+ def lemma[A](xs: List[A], n: BigInt) =
+ (lenTailrec(xs, n) >= n).holds
+
+The attribute ``[[leon_induct _]]`` summons the induction rule for the
+specified function.
+
+
+Limitations
+-----------
+
+ - Mutually-recursive datatypes must be "homogeneous", that is, they all must
+ have exactly the same type parameters; otherwise, they cannot be translated.
+ - Recursive functions must have at least one declared parameter.
+ - Polymorphic recursion is unsupported.
+ - The ``const`` and ``leon_induct`` syntax take a mangled identifier name,
+ according to the name mangling rules of Scala (and some additional ones).
+ The mangling doesn't change the name if it only contains alphanumeric
+ characters.
+ - The ``const`` and ``leon_induct`` syntax does not work for a given function
+ ``f`` if there is another function ``f`` defined anywhere else in the
+ program.
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index d1e7f3f3f12213829ad4703088b1a843741d2426..492c3e3b4c31d2d73c7eab3ab2bf36648dbd7f18 100644
--- a/src/sphinx/options.rst
+++ b/src/sphinx/options.rst
@@ -166,6 +166,10 @@ These options are available by all Leon components:
* ``ground``
Only solves ground verification conditions (without variables) by evaluating them.
+
+ * ``isabelle``
+
+ Solve verification conditions via Isabelle.
* ``--strict``
@@ -182,7 +186,7 @@ These options are available by all Leon components:
Support for additional language constructs described in :ref:`xlang`.
These constructs are desugared into :ref:`purescala` before other operations.
-Additional Options, by Component:
+Additional Options (by component)
---------------------------------
File Output
@@ -193,7 +197,7 @@ File Output
Output files to the directory ``dir`` (default: leon.out).
Used when ``--noop`` is selected.
-Code extraction
+Code Extraction
***************
* ``--strictCompilation``
@@ -240,6 +244,7 @@ These options are also used by repair during the synthesis stage.
Fair-z3 Solver
**************
+
* ``--checkmodels``
Double-check counter-examples with evaluator.
@@ -260,9 +265,52 @@ Fair-z3 Solver
Use unsat-cores to drive unrolling while remaining fair.
-CVC4-solver
+CVC4 Solver
***********
* ``--solver:cvc4=<cvc4-opt>``
Pass extra command-line arguments to CVC4.
+
+Isabelle
+********
+
+* ``--isabelle:base=<path>``
+
+ Specify the installation directory of Isabelle. In Isabelle-parlance, this is
+ called ``$ISABELLE_HOME``. It will have the form ``/path/to/Isabelle2015``.
+ When no Isabelle installation can be found there, the system suggests to
+ enable the ``download`` option.
+
+* ``--isabelle:build``
+
+ Flag to indicate that during the start-up of Leon, Isabelle should
+ automatically build all required library sources. This is on by default, and
+ should usually be left on. Building only happens when some dependencies
+ changed and subsequent runs of Leon don't rebuild the library. However, even
+ if nothing is build, it still requires the system a couple of seconds to
+ figure that out.
+
+* ``--isabelle:download``
+
+ If necessary, perform a full system bootstrap by downloading and unpacking a
+ copy of Isabelle. Off by default. Only supported under Linux.
+
+* ``--isabelle:dump=<path>``
+
+ Makes the system write theory files containing the translated definitions
+ and scripts. The generated files may be loaded directly into Isabelle, but
+ are not guaranteed to work, as pretty-printing Isabelle terms is only an
+ approximation.
+
+* ``--isabelle:mapping``
+
+ Controls function and type mapping. On by default. When switched off, neither
+ functions nor types are mapped at all.
+
+* ``--isabelle:strict``
+
+ Strict prover mode. On by default. Replays all referenced proofs from the
+ library when verifiying a Leon source file. Keeping it enabled prevents
+ unsound proofs when postconditions or mappings in the library are wrong.
+ When disabled, a warning is printed.
diff --git a/src/sphinx/purescala.rst b/src/sphinx/purescala.rst
index 450abf271d976da1dfc836727c2eb0326347eaef..ee41a7ec83a68ff479b2316b9085b5302c017237 100644
--- a/src/sphinx/purescala.rst
+++ b/src/sphinx/purescala.rst
@@ -3,8 +3,8 @@
Pure Scala
==========
-The input to Leon is a purely functional **subset** of Scala
-(http://www.scala-lang.org/), which we call
+The input to Leon is a purely functional **subset** of `Scala
+<http://www.scala-lang.org/>`_, which we call
**Pure Scala**. Constructs specific for Leon are defined inside
Leon's libraries in package `leon` and its subpackages. Leon
invokes standard `scalac` compiler on the input file, then
diff --git a/src/sphinx/references.rst b/src/sphinx/references.rst
index c7c4f2b8a0d8f32b42ba0395cf0fb1fec900b678..951579cfafc23929a1bf7f3481c44ac0749358a9 100644
--- a/src/sphinx/references.rst
+++ b/src/sphinx/references.rst
@@ -32,3 +32,9 @@ Papers
- `Decision Procedures for Algebraic Data Types with Abstractions <http://lara.epfl.ch/~kuncak/papers/SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions.pdf>`_, by *Philippe Suter*, *Mirco Dotta*, *Viktor Kuncak*. Principles of Programming Languages (POPL), 2010
- `Complete functional synthesis <http://lara.epfl.ch/~kuncak/papers/KuncakETAL10CompleteFunctionalSynthesis.pdf>`_, by *Viktor Kuncak*, *Mikael Mayer*, *Ruzica Piskac*, and *Philippe Suter*. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2010.
+
+
+Books
+*****
+
+ - `Concrete Sematics with Isabelle/HOL <http://www.concrete-semantics.org/>`_, by *Tobias Nipkow* and *Gerwin Klein*.