diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst index d18afc8cf01404e8981363818455188b90ced9f5..4eff3598fcb3c86a92dd0f4025c91db30a3b74eb 100644 --- a/doc/gettingstarted.rst +++ b/doc/gettingstarted.rst @@ -93,7 +93,8 @@ and get something like this For more details on how to build Leon from sources that can be used directly from the shell, see -:ref:`installation`. +:ref:`installation`. In addition to invoking `./leon --help` you +may wish to consult :ref:`cmdlineoptions`. Asking Questions diff --git a/doc/installation.rst b/doc/installation.rst index ed94551144890b565f803b31702436bbd6cc1839..278a696fcd85d3fcfa76de8861ac22d65b224ce8 100644 --- a/doc/installation.rst +++ b/doc/installation.rst @@ -88,20 +88,5 @@ In any case, we recommend that you install both solvers separately and have 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 the -the ``--solvers`` command line option: - -:: - - --solvers=s1,s2 Use solvers s1 and s2 - Available: - enum : Enumeration-based counter-example-finder - fairz3 : Native Z3 with z3-templates for unfolding (default) - smt-cvc4 : CVC4 through SMT-LIB - smt-cvc4-cex : CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only - smt-cvc4-proof : CVC4 through SMT-LIB, in-solver inductive reasonning, for proofs only - smt-z3 : Z3 through SMT-LIB - smt-z3-q : Z3 through SMT-LIB, with quantified encoding - unrollz3 : Native Z3 with leon-templates for unfolding - - +specify another solver if this native layer is not available to you. Check also the +the ``--solvers`` in :ref:`cmdlineoptions` . diff --git a/doc/options.rst b/doc/options.rst index b9661bdb471405c64f5fa7d86736b951df53d1c9..b4462aa13d1809a34a48f517890e0a0319c1144e 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -1,10 +1,12 @@ +.. _cmdlineoptions: + Command Line Options ==================== Here is an overview of the command-line options that Leon recognizes: -Choosing the feature to use: ----------------------------- +Choosing the feature to use +--------------------------- The first group of options determine which feature of Leon will be used. They are mutually exclusive, with ``--verify`` being the default. diff --git a/doc/purescala.rst b/doc/purescala.rst index 4875e73eb939d5030c91870da3b14ccd4b379978..b8236f09e459598e5a7a410d18291dc1a5eb342d 100644 --- a/doc/purescala.rst +++ b/doc/purescala.rst @@ -1,7 +1,7 @@ .. _purescala: -Pure Scala: Leon's Language -=========================== +Pure Scala +========== The input to Leon is a purely functional subset of Scala, which we call **Pure Scala**. Constructs specific for Leon diff --git a/doc/tutorial.rst b/doc/tutorial.rst index 467c48abacc66785573c0f67775256ba44ea8368..f4dce6b9541320b72e0f7ffecc776151a6d53454 100644 --- a/doc/tutorial.rst +++ b/doc/tutorial.rst @@ -1,22 +1,22 @@ .. _tutorial: -Tutorials -========= +Tutorial: Sorting +================= -For these tutorials we occasionally assume that the user is using the web -interface. The functionality is also available (possibly with less -convenient interface) from the command line, see :ref:`gettingstarted`. +This tutorial shows how to: -Sorting Lists -------------- + * define lists as algebraic data types + * specify sortedness of a list and use function contracts + * verify properties of an insertion into a sorted list + * execute or synthesize provably correct operations using specifications alone, + without the need to write implementation -This tutorial shows how to define lists as algebraic data -types, how to **verify** certain properties of an insertion -sort. We finish showing how to use Leon to **synthesize** -provably correct operations from specifications. +For this tutorial we occasionally assume that the user is using the web +interface. The functionality is also available (possibly with less +convenient interface) from the command line, see :ref:`gettingstarted`. -A Preview of Specification and Synthesis -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Sorting Two Elements +-------------------- As a preview, let us start by **specifying** a function that sorts **two** mathematical integers. Here is what we need @@ -82,7 +82,7 @@ length two. Note that the result is uniquely specified, no matter what the values of `x` and `y` are. Evaluating exppressions containing choose -......................................... +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Leon contains a built-in evaluator. To see it in action in the web interface, just define a function without @@ -105,7 +105,7 @@ more efficient code. Leon can automate this process in some cases, using **synthesis**. Synthesizing the sort of two elements -..................................... +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Instead of executing `choose` using a constraint solver during execution, we can alternatively instruct Leon to @@ -139,13 +139,13 @@ satisfies our specification. In this case, the specification is unambiguous, so all programs that one can synthesize compute the same results for all inputs. -Defining lists -^^^^^^^^^^^^^^ +Defining Unbounded Lists +------------------------ Let us now consider sorting of any number of elements. For this purpose, we define the data structure of lists of -(big) integers. (Leon has a built-in data type of +(big) integers. Leon has a built-in data type of polymorphic lists, see :ref:`Leon Library <library>`, but -here we will define our own variant.) +here we define our own variant.