diff --git a/src/sphinx/.gitignore b/src/sphinx/.gitignore
deleted file mode 100644
index e35d8850c9688b1ce82711694692cc574a799396..0000000000000000000000000000000000000000
--- a/src/sphinx/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-_build
diff --git a/src/sphinx/Makefile b/src/sphinx/Makefile
deleted file mode 100644
index 5fd9401a6354dd9d9f813d294ac577c1ca4c0c93..0000000000000000000000000000000000000000
--- a/src/sphinx/Makefile
+++ /dev/null
@@ -1,177 +0,0 @@
-# Makefile for Sphinx documentation
-#
-
-# You can set these variables from the command line.
-SPHINXOPTS =
-SPHINXBUILD = sphinx-build
-PAPER =
-BUILDDIR = _build
-
-# User-friendly check for sphinx-build
-ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
-$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from http://sphinx-doc.org/)
-endif
-
-# Internal variables.
-PAPEROPT_a4 = -D latex_paper_size=a4
-PAPEROPT_letter = -D latex_paper_size=letter
-ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
-# the i18n builder cannot share the environment and doctrees with the others
-I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
-
-.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest gettext
-
-help:
- @echo "Please use \`make <target>' where <target> is one of"
- @echo " html to make standalone HTML files"
- @echo " dirhtml to make HTML files named index.html in directories"
- @echo " singlehtml to make a single large HTML file"
- @echo " pickle to make pickle files"
- @echo " json to make JSON files"
- @echo " htmlhelp to make HTML files and a HTML help project"
- @echo " qthelp to make HTML files and a qthelp project"
- @echo " devhelp to make HTML files and a Devhelp project"
- @echo " epub to make an epub"
- @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
- @echo " latexpdf to make LaTeX files and run them through pdflatex"
- @echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
- @echo " text to make text files"
- @echo " man to make manual pages"
- @echo " texinfo to make Texinfo files"
- @echo " info to make Texinfo files and run them through makeinfo"
- @echo " gettext to make PO message catalogs"
- @echo " changes to make an overview of all changed/added/deprecated items"
- @echo " xml to make Docutils-native XML files"
- @echo " pseudoxml to make pseudoxml-XML files for display purposes"
- @echo " linkcheck to check all external links for integrity"
- @echo " doctest to run all doctests embedded in the documentation (if enabled)"
-
-clean:
- rm -rf $(BUILDDIR)/*
-
-html:
- $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
- @echo
- @echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
-
-dirhtml:
- $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
- @echo
- @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
-
-singlehtml:
- $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
- @echo
- @echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
-
-pickle:
- $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
- @echo
- @echo "Build finished; now you can process the pickle files."
-
-json:
- $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
- @echo
- @echo "Build finished; now you can process the JSON files."
-
-htmlhelp:
- $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
- @echo
- @echo "Build finished; now you can run HTML Help Workshop with the" \
- ".hhp project file in $(BUILDDIR)/htmlhelp."
-
-qthelp:
- $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
- @echo
- @echo "Build finished; now you can run "qcollectiongenerator" with the" \
- ".qhcp project file in $(BUILDDIR)/qthelp, like this:"
- @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/Leon.qhcp"
- @echo "To view the help file:"
- @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/Leon.qhc"
-
-devhelp:
- $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
- @echo
- @echo "Build finished."
- @echo "To view the help file:"
- @echo "# mkdir -p $$HOME/.local/share/devhelp/Leon"
- @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/Leon"
- @echo "# devhelp"
-
-epub:
- $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
- @echo
- @echo "Build finished. The epub file is in $(BUILDDIR)/epub."
-
-latex:
- $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
- @echo
- @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
- @echo "Run \`make' in that directory to run these through (pdf)latex" \
- "(use \`make latexpdf' here to do that automatically)."
-
-latexpdf:
- $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
- @echo "Running LaTeX files through pdflatex..."
- $(MAKE) -C $(BUILDDIR)/latex all-pdf
- @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
-
-latexpdfja:
- $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
- @echo "Running LaTeX files through platex and dvipdfmx..."
- $(MAKE) -C $(BUILDDIR)/latex all-pdf-ja
- @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
-
-text:
- $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
- @echo
- @echo "Build finished. The text files are in $(BUILDDIR)/text."
-
-man:
- $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
- @echo
- @echo "Build finished. The manual pages are in $(BUILDDIR)/man."
-
-texinfo:
- $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
- @echo
- @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
- @echo "Run \`make' in that directory to run these through makeinfo" \
- "(use \`make info' here to do that automatically)."
-
-info:
- $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
- @echo "Running Texinfo files through makeinfo..."
- make -C $(BUILDDIR)/texinfo info
- @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
-
-gettext:
- $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
- @echo
- @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
-
-changes:
- $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
- @echo
- @echo "The overview file is in $(BUILDDIR)/changes."
-
-linkcheck:
- $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
- @echo
- @echo "Link check complete; look for any errors in the above output " \
- "or in $(BUILDDIR)/linkcheck/output.txt."
-
-doctest:
- $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
- @echo "Testing of doctests in the sources finished, look at the " \
- "results in $(BUILDDIR)/doctest/output.txt."
-
-xml:
- $(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml
- @echo
- @echo "Build finished. The XML files are in $(BUILDDIR)/xml."
-
-pseudoxml:
- $(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml
- @echo
- @echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml."
diff --git a/src/sphinx/conf.py b/src/sphinx/conf.py
deleted file mode 100644
index de027efc1654c02de394ab978e07c37987070823..0000000000000000000000000000000000000000
--- a/src/sphinx/conf.py
+++ /dev/null
@@ -1,274 +0,0 @@
-# -*- coding: utf-8 -*-
-#
-# Leon documentation build configuration file, created by
-# sphinx-quickstart on Fri Feb 27 13:23:31 2015.
-#
-# This file is execfile()d with the current directory set to its
-# containing dir.
-#
-# Note that not all possible configuration values are present in this
-# autogenerated file.
-#
-# All configuration values have a default; values that are commented out
-# serve to show the default.
-
-import sys
-import os
-
-docauthorlist = u'M. Antognini, R. Blanc, S. Gruetter, L. Hupel, E. Kneuss, M. Koukoutos, V. Kuncak, S. Stucki, P. Suter'
-
-# If extensions (or modules to document with autodoc) are in another directory,
-# add these directories to sys.path here. If the directory is relative to the
-# documentation root, use os.path.abspath to make it absolute, like shown here.
-#sys.path.insert(0, os.path.abspath('.'))
-
-# -- General configuration ------------------------------------------------
-
-# If your documentation needs a minimal Sphinx version, state it here.
-#needs_sphinx = '1.0'
-
-# Add any Sphinx extension module names here, as strings. They can be
-# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
-# ones.
-extensions = [
- 'sphinx.ext.todo',
- 'sphinx.ext.mathjax',
-]
-
-mathjax_path = 'https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML'
-
-# Add any paths that contain templates here, relative to this directory.
-templates_path = ['_templates']
-
-# The suffix of source filenames.
-source_suffix = '.rst'
-
-# The encoding of source files.
-#source_encoding = 'utf-8-sig'
-
-# The master toctree document.
-master_doc = 'index'
-
-# General information about the project.
-project = u'Leon'
-copyright = u'2015 (alphabetically) by ' + docauthorlist
-
-# The version info for the project you're documenting, acts as replacement for
-# |version| and |release|, also used in various other places throughout the
-# built documents.
-#
-# The short X.Y version.
-version = '3.0'
-# The full version, including alpha/beta/rc tags.
-release = '3.0'
-
-# The language for content autogenerated by Sphinx. Refer to documentation
-# for a list of supported languages.
-#language = None
-
-# There are two options for replacing |today|: either, you set today to some
-# non-false value, then it is used:
-#today = ''
-# Else, today_fmt is used as the format for a strftime call.
-#today_fmt = '%B %d, %Y'
-
-# List of patterns, relative to source directory, that match files and
-# directories to ignore when looking for source files.
-exclude_patterns = ['_build']
-
-# The reST default role (used for this markup: `text`) to use for all
-# documents.
-#default_role = None
-
-# If true, '()' will be appended to :func: etc. cross-reference text.
-#add_function_parentheses = True
-
-# If true, the current module name will be prepended to all description
-# unit titles (such as .. function::).
-#add_module_names = True
-
-# If true, sectionauthor and moduleauthor directives will be shown in the
-# output. They are ignored by default.
-show_authors = False
-
-# The name of the Pygments (syntax highlighting) style to use.
-#pygments_style = 'trac'
-
-# A list of ignored prefixes for module index sorting.
-#modindex_common_prefix = []
-
-# If true, keep warnings as "system message" paragraphs in the built documents.
-#keep_warnings = False
-
-
-# -- Options for HTML output ----------------------------------------------
-
-# The theme to use for HTML and HTML Help pages. See the documentation for
-# a list of builtin themes.
-html_theme = 'leon'
-
-# Theme options are theme-specific and customize the look and feel of a theme
-# further. For a list of options available for each theme, see the
-# documentation.
-html_theme_options = {
- "headerbg": '#19214F !important',
- "footerbg": '#19214F !important',
- "linkcolor": '#2980B9',
- "headerlinkcolor": '#6CA2C5',
- "headerfont": 'Arial, sans-serif',
- "bodyfont": 'Arial, sans-serif',
- "headercolor1": "#19214F",
- "headercolor2": "#19214F",
-}
-
-# Add any paths that contain custom themes here, relative to this directory.
-html_theme_path = ["themes"]
-
-# The name for this set of Sphinx documents. If None, it defaults to
-# "<project> v<release> documentation".
-#html_title = None
-
-# A shorter title for the navigation bar. Default is the same as html_title.
-html_short_title = "Leon Documentation"
-
-# The name of an image file (relative to this directory) to place at the top
-# of the sidebar.
-#html_logo = None
-
-# The name of an image file (within the static path) to use as favicon of the
-# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
-# pixels large.
-#html_favicon = None
-
-# Add any paths that contain custom static files (such as style sheets) here,
-# relative to this directory. They are copied after the builtin static files,
-# so a file named "default.css" will overwrite the builtin "default.css".
-#html_static_path = ['_static']
-
-# Add any extra paths that contain custom files (such as robots.txt or
-# .htaccess) here, relative to this directory. These files are copied
-# directly to the root of the documentation.
-#html_extra_path = []
-
-# If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
-# using the given strftime format.
-html_last_updated_fmt = '%b %d, %Y'
-
-# If true, SmartyPants will be used to convert quotes and dashes to
-# typographically correct entities.
-#html_use_smartypants = True
-
-# Custom sidebar templates, maps document names to template names.
-#html_sidebars = {}
-
-# Additional templates that should be rendered to pages, maps page names to
-# template names.
-#html_additional_pages = {}
-
-# If false, no module index is generated.
-#html_domain_indices = True
-
-# If false, no index is generated.
-#html_use_index = True
-
-# If true, the index is split into individual pages for each letter.
-#html_split_index = False
-
-# If true, links to the reST sources are added to the pages.
-#html_show_sourcelink = True
-
-# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
-html_show_sphinx = False
-
-# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
-html_show_copyright = True
-
-# If true, an OpenSearch description file will be output, and all pages will
-# contain a <link> tag referring to it. The value of this option must be the
-# base URL from which the finished HTML is served.
-#html_use_opensearch = ''
-
-# This is the file name suffix for HTML files (e.g. ".xhtml").
-#html_file_suffix = None
-
-# Output file base name for HTML help builder.
-htmlhelp_basename = 'Leondoc'
-
-
-# -- Options for LaTeX output ---------------------------------------------
-
-latex_elements = {
-# The paper size ('letterpaper' or 'a4paper').
-#'papersize': 'letterpaper',
-
-# The font size ('10pt', '11pt' or '12pt').
-#'pointsize': '10pt',
-
-# Additional stuff for the LaTeX preamble.
-#'preamble': '',
-}
-
-# Grouping the document tree into LaTeX files. List of tuples
-# (source start file, target name, title,
-# author, documentclass [howto, manual, or own class]).
-latex_documents = [
- ('index', 'Leon.tex', u'Leon Documentation',
- docauthorlist, 'manual'),
-]
-
-# The name of an image file (relative to this directory) to place at the top of
-# the title page.
-#latex_logo = None
-
-# For "manual" documents, if this is true, then toplevel headings are parts,
-# not chapters.
-#latex_use_parts = False
-
-# If true, show page references after internal links.
-#latex_show_pagerefs = False
-
-# If true, show URL addresses after external links.
-#latex_show_urls = False
-
-# Documents to append as an appendix to all manuals.
-#latex_appendices = []
-
-# If false, no module index is generated.
-#latex_domain_indices = True
-
-
-# -- Options for manual page output ---------------------------------------
-
-# One entry per manual page. List of tuples
-# (source start file, name, description, authors, manual section).
-man_pages = [
- ('index', 'leon', u'Leon Documentation',
- [docauthorlist], 1)
-]
-
-# If true, show URL addresses after external links.
-#man_show_urls = False
-
-
-# -- Options for Texinfo output -------------------------------------------
-
-# Grouping the document tree into Texinfo files. List of tuples
-# (source start file, target name, title, author,
-# dir menu entry, description, category)
-texinfo_documents = [
- ('index', 'Leon', u'Leon Documentation',
- copyright, 'One line description of project.',
- 'Miscellaneous'),
-]
-
-# Documents to append as an appendix to all manuals.
-#texinfo_appendices = []
-
-# If false, no module index is generated.
-#texinfo_domain_indices = True
-
-# How to display URL addresses: 'footnote', 'no', or 'inline'.
-#texinfo_show_urls = 'footnote'
-
-# If true, do not generate a @detailmenu in the "Top" node's menu.
-#texinfo_no_detailmenu = False
diff --git a/src/sphinx/faq.rst b/src/sphinx/faq.rst
deleted file mode 100644
index cb45de8b8623d9190bec1ff8c90c3d52d84dd0da..0000000000000000000000000000000000000000
--- a/src/sphinx/faq.rst
+++ /dev/null
@@ -1,101 +0,0 @@
-.. _faq:
-
-Frequently Asked Questions
-==========================
-
-If you have a question, we suggest you post it at http://stackoverflow.com
-(try `searching for the leon tag <http://stackoverflow.com/questions/tagged/leon?sort=newest>`_)
-or contact one of the authors of this documentation.
-
-Below we collect answers to some questions that came up.
-
-Proving properties of size
-^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-I have defined a size function on my algebraic data type.
-
-.. code-block:: scala
-
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case object Nil extends List
- def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
- }) ensuring(_ >= 0)
-
-Leon neither proves nor gives a counterexample. Why?
-
-**Answer:** You should consider using `BigInt`, which
-denotes unbounded mathematical integers, instead of `Int`,
-which denotes 32-bit integers. If you replace `Int` with
-`BigInt` in the result type of `size`, the function should
-verify. Note that algebraic data types can be arbitrarily
-large, so, if the input list had the size `Int.MaxValue + 1`
-(which is 2^32) then the addition `1 + size(t)` would wrap
-around and produce `Int.MinValue` (that is, -2^31), so the
-`ensuring` clause would not hold.
-
-Use variable number of arguments in Leon programs
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-I have defined an apply function that should accept a variable number of arguments.
-
-.. code-block:: scala
-
- import leon.collection._
- case class Element(children: List[Element]) {
- def addChildren(c: Element*): Element = {
- Element(children ++ c.toList)
- }
- }
-
-This does not compile in Leon, why?
-
-**Answer:**
-
-To support variable number of arguments, do the following:
-
-.. code-block:: scala
-
- import leon.collection._
- import leon.annotation._
- case class Element(children: List[Element]) {
- @ignore
- def addChildren(c: Element*): Element = {
- var l: List[WebTree] = Nil[WebTree]()
- for (e <- elems) {
- l = Cons(e, l)
- }
- addChildren(l.reverse)
- }
- def addChildren(c: List[Element]): Element = {
- Element(children ++ toList)
- }
- }
-
-This code is compatible with both Leon and Scala.
-At parsing time, when Leon encounters a call to
-`addChildren(a, b)`
-using the first method, it translates it to
-`addChildren(Cons(a, Cons(b, Nil())))`
-using the second method.
-When Scala encounters the same call,
-it executes the `@ignore`-d function and calls the second method.
-
-The reason is that the `scala.collection.Seq` used in the case of multiple arguments does not have a method `toList` that converts the sequence to a Leon `List`. Hence this workaround.
-
-Compiling Leon programs to bytecode
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-If you don't use special constructs such as ``choose``, you should be able to
-compile Leon programs to `.class` using `scalac` and execute them directly on
-the JVM, or integrate them as part as other Scala-based projects.
-
-Beware that you need to explicitly include files files from the Leon library
-(that are implicitly bundled when you use the `./leon` script):
-
-.. code-block:: bash
-
- $ mkdir out
- $ scalac $(find path/to/leon/library/ -name "*.scala" | xargs) MyFile.scala -d out
diff --git a/src/sphinx/genc.rst b/src/sphinx/genc.rst
deleted file mode 100644
index faac1f142f843e4014dbac4603784c4fa37ebe16..0000000000000000000000000000000000000000
--- a/src/sphinx/genc.rst
+++ /dev/null
@@ -1,122 +0,0 @@
-.. _genc:
-
-Safe C Code
-===========
-
-Leon can generate from Scala code an equivalent and safe C99 code. Using the verification, repair and
-synthesis features of Leon this conversion can be made safely. Additionally, the produced code can be
-compiled with any standard-compliant C99 compiler to target the desired hardware architecture
-without extra dependencies.
-
-To convert a Scala program, one can use the ``--genc`` and ``--o=<output.c>`` command line options
-of Leon.
-
-.. NOTE::
- Currently the memory model is limited to stack-allocated memory. Hence, no dynamic allocation
- is done using ``malloc`` function family.
-
-
-Supported Features
-------------------
-
-The supported subset of Scala includes part of the core languages features, as well as some
-extensions from :ref:`XLang <xlang>`, while ensuring the same expression execution order in both
-languages.
-
-Currently all type and function definitions need to be included in one top level object.
-
-
-Types
-*****
-
-The following raw types and their corresponding literals are supported:
-
-.. list-table::
- :header-rows: 1
-
- * - Scala
- - C99
- * - ``Unit``
- - ``void``
- * - ``Boolean``
- - ``bool``
- * - ``Int`` (32-bit Integer)
- - ``int32_t``
-
-Tuples
-^^^^^^
-
-Using ``TupleN[T1, ..., TN]`` results in the creation of a C structure with the same
-fields and types for every combination of any supported type ``T1, ..., TN``. The name of the
-generated structure will be unique and reflect the sequence of types.
-
-
-Arrays
-^^^^^^
-
-``Array[T]`` are implemented using regular C array when the array size is known at compile time, or
-using Variable Length Array (VLA) when the size is only available at runtime. Both types of array
-use the same unique structure type to keep track of the length of the array and its allocated
-memory.
-
-.. NOTE::
-
- Arrays live on the stack and therefore cannot be returned by functions. This limitation is
- extended to other types having an array as field.
-
-
-Arrays can be created using the companion object, e.g. ``Array(1, 2, 3)``, or using the
-``Array.fill`` method, e.g. ``Array.fill(size)(value)``.
-
-
-Case Classes
-^^^^^^^^^^^^
-
-The support for classes is restricted to non-recursive case classes for which fields are immutable.
-Instances of such data-types live on the stack.
-
-
-Functions
-*********
-
-Functions and nested functions are supported, with access to the variables in their respective
-scopes. However, higher order functions are as of this moment not supported.
-
-Since strings of characters are currently not available, to generate an executable program, one has
-to define a main function without any argument that returns an integer: ``def main: Int = ...``.
-
-Both ``val`` and ``var`` are supported with the limitations imposed by the :ref:`XLang <xlang>`
-extensions.
-
-
-Constructs
-**********
-
-The idiomatic ``if`` statements such as ``val b = if (x >= 0) true else false`` are converted into
-a sequence of equivalent statements.
-
-Imperative ``while`` loops are also supported.
-
-Assertions, invariant, pre- and post-conditions are not translated into C99 and are simply ignored.
-
-
-Operators
-*********
-
-The following operators are supported:
-
-.. list-table::
- :header-rows: 1
-
- * - Category
- - Operators
- * - Boolean operators
- - ``&&``, ``||``, ``!``, ``!=``, ``==``
- * - Comparision operators over integers
- - ``<``, ``<=``, ``==``, ``!=``, ``>=``, ``>``
- * - Arithmetic operators over integers
- - ``+``, ``-`` (unary & binary), ``*``, ``/``, ``%``
- * - Bitwise operators over integers
- - ``&``, ``|``, ``^``, ``~``, ``<<``, ``>>``
-
-
diff --git a/src/sphinx/gettingstarted.rst b/src/sphinx/gettingstarted.rst
deleted file mode 100644
index 2e5576d1df3f80eefc9fd97cc12dba1491b23d16..0000000000000000000000000000000000000000
--- a/src/sphinx/gettingstarted.rst
+++ /dev/null
@@ -1,103 +0,0 @@
-.. _gettingstarted:
-
-Getting Started
-===============
-
-Web Interface
--------------
-
-The simplest way to try out Leon is to use it through the
-web interface http://leon.epfl.ch. The web interface uses
-standard Javascript and should run in most browsers,
-including Chrome and Firefox.
-
-The web interface requires you to enter your entire program
-into the single web editor buffer. For example, you can
-paste into the editor the definition of the following `max`
-function on unbounded integers:
-
-.. code-block:: scala
-
- object Max {
- def max(x: BigInt, y: BigInt): BigInt = {
- if (x <= y) y
- else x
- } ensuring(res => x <= res && y <= res)
- }
-
-The above program should verify. If you change `y <= res`
-into `y < res`, Leon should report a counterexample; try
-clicking on the names of parameters `x` and `y` as well
-as various parts in the `ensuring` clause.
-
-You can also **select from a number of provided examples**,
-and then edit them subsequently. Selecting a different
-sample program from the web interface will erase the
-previously entered program.
-
-The web interface fixes particular settings including the
-timeout values for verification and synthesis tasks. For
-longer tasks we currently recommend using the command line.
-
-Command Line
-------------
-
-Leon can be used as a command line tool, which exposes most
-of the functionality. To see the main options, use
-
-.. code-block:: bash
-
- ./leon --help
-
-in your command line shell while in the top-level Leon directory.
-
-You can try some of the examples from the `testcases/` directory
-distributed with Leon:
-
-.. code-block:: bash
-
- $ ./leon --solvers=smt-cvc4 ./testcases/verification/sas2011-testcases/RedBlackTree.scala
-
-and get something like this
-
-.. code-block:: bash
-
- ┌──────────────────────┐
- ╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
- ║ └──────────────────────┘ ║
- ║ add postcondition 82:15 valid U:smt-cvc4 0.258 ║
- ║ add precondition 81:15 valid U:smt-cvc4 0.007 ║
- ║ add precondition 81:5 valid U:smt-cvc4 0.049 ║
- ║ balance match exhaustiveness 90:5 valid U:smt-cvc4 0.006 ║
- ║ balance postcondition 101:15 valid U:smt-cvc4 0.301 ║
- ║ blackBalanced match exhaustiveness 45:43 valid U:smt-cvc4 0.006 ║
- ║ blackHeight match exhaustiveness 50:40 valid U:smt-cvc4 0.009 ║
- ║ buggyAdd postcondition 87:15 invalid U:smt-cvc4 1.561 ║
- ║ buggyAdd precondition 86:5 invalid U:smt-cvc4 0.135 ║
- ║ buggyBalance match exhaustiveness 104:5 invalid U:smt-cvc4 0.008 ║
- ║ buggyBalance postcondition 115:15 invalid U:smt-cvc4 0.211 ║
- ║ content match exhaustiveness 17:37 valid U:smt-cvc4 0.030 ║
- ║ ins match exhaustiveness 59:5 valid U:smt-cvc4 0.007 ║
- ║ ins postcondition 66:15 valid U:smt-cvc4 3.996 ║
- ║ ins precondition 62:37 valid U:smt-cvc4 0.034 ║
- ║ ins precondition 64:40 valid U:smt-cvc4 0.036 ║
- ║ makeBlack postcondition 77:14 valid U:smt-cvc4 0.036 ║
- ║ redDescHaveBlackChildren match exhaustiveness 40:53 valid U:smt-cvc4 0.005 ║
- ║ redNodesHaveBlackChildren match exhaustiveness 34:54 valid U:smt-cvc4 0.007 ║
- ║ size match exhaustiveness 22:33 valid U:smt-cvc4 0.005 ║
- ║ size postcondition 25:15 valid U:smt-cvc4 0.055 ║
- ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
- ║ total: 21 valid: 17 invalid: 4 unknown 0 6.762 ║
- ╚════════════════════════════════════════════════════════════════════════════════════════════╝
-
-
-For more details on how to build Leon from sources that can
-be used directly from the shell, see
-:ref:`installation`. In addition to invoking `./leon --help` you
-may wish to consult :ref:`cmdlineoptions` options.
-
-Some benchmarks may contain Scala code that is ignored by verifier, but contributes
-to running the benchmark. To start a Leon program with Scala, just compile it together
-with Leon libraries inside the `library/` directory of Leon distribution. The scripts
-`scalacleon` and `scalaleon` attempt to automate this for simple cases and need to be
-invoked from the Leon installation directory.
diff --git a/src/sphinx/index.rst b/src/sphinx/index.rst
deleted file mode 100644
index cf46d2c300d3821a4cb987d657bded60597ce534..0000000000000000000000000000000000000000
--- a/src/sphinx/index.rst
+++ /dev/null
@@ -1,39 +0,0 @@
-.. Leon documentation master file, created by
- sphinx-quickstart on Fri Feb 27 13:23:31 2015.
- You can adapt this file completely to your liking, but it should at least
- contain the root `toctree` directive.
-
-Leon documentation
-==================
-
-Contents:
-
-.. toctree::
- :maxdepth: 2
-
- intro
- gettingstarted
- installation
- tutorial
- purescala
- library
- xlang
- verification
- invinference
- neon
- isabelle
- limitations
- synthesis
- repair
- genc
- options
- faq
- references
-
-
-Indices and tables
-==================
-
-* :ref:`genindex`
-* :ref:`search`
-
diff --git a/src/sphinx/installation.rst b/src/sphinx/installation.rst
deleted file mode 100644
index b4deaf194eb4f84eac0b14dabb42221cfb999056..0000000000000000000000000000000000000000
--- a/src/sphinx/installation.rst
+++ /dev/null
@@ -1,224 +0,0 @@
-.. _installation:
-
-Installing Leon
-===============
-
-Leon requires quite a few dependencies, and you will need to
-make sure everything is correctly set up before being able
-to build it. Leon is probably easiest to build on Linux-like
-platforms, but read on regarding other platforms.
-
-Due to its nature, this documentation section may not always
-be up to date; we welcome pull requests with carefully
-written and tested improvements to the information below.
-
-**Requirements:**
-
-* `Java SE Development Kit 8 <http://www.oracle.com/technetwork/java/javase/downloads/jdk8-downloads-2133151.html>`_ or `Java SE Development Kit 7 <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_ for your platform
-* SBT 0.13.x (Available from http://www.scala-sbt.org/)
-* Support for at least one external solver (See :ref:`smt-solvers`)
-* `Sphinx restructured text tool <http://sphinx-doc.org/>`_ (for building local documentation)
-
-Linux & Mac OS-X
-----------------
-
-Get the sources of Leon by cloning the official Leon repository:
-
-.. code-block:: bash
-
- $ git clone https://github.com/epfl-lara/leon.git
- Cloning into 'leon'...
- // ...
- $ cd leon
- $ sbt clean compile
- // takes about 3 minutes
-
-We now use ``sbt script`` to create a ``leon`` bash script that runs Leon with
-all the appropriate settings:
-
-.. code-block:: bash
-
- $ sbt script
- $ ./leon --help
-
-Note that Leon is organized as a structure of several
-projects, with a main (or root) project and at least one
-sub-project. From a user point of view, this should most of
-the time be transparent and the build command should take
-care of everything.
-
-Windows
--------
-
-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
-
- $ git clone https://github.com/epfl-lara/leon.git
- Cloning into 'leon'...
- // ...
- $ cd leon
- $ sbt clean compile
- // takes about 3 minutes
-
-We now use ``sbt script`` to create a ``leon`` bash script that runs leon with
-all the appropriate settings:
-
-.. code-block:: bash
-
- $ sbt script
-
-You will now need to either port the bash script to Windows, or to run it
-under Cygwin.
-
-**Known issues**
-
-*Missing jars*
-
-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/``
-
-You may be able to obtain additional tips on getting Leon to work on Windows
-from [Mikael Mayer](http://people.epfl.ch/mikael.mayer) or on [his dedicated web page](http://lara.epfl.ch/~mayer/leon/),
-
-.. _smt-solvers:
-
-External Solvers
-----------------
-
-Leon typically relies on external (SMT) solvers to solve the constraints it generates.
-
-We currently support two major SMT solvers:
-
- * CVC4, http://cvc4.cs.nyu.edu/web/
- * Z3, https://github.com/Z3Prover/z3
-
-Solver binaries that you install should match your operating
-system and your architecture. We recommend that you install
-these solvers as a binary and have their binaries available
-in the ``$PATH``. Once they are installed, you can instruct
-Leon to use a given sequence of solvers. The more solvers
-you have installed, the more successful Leon might get,
-because solver capabilities are incomparable.
-
-In addition to these external binaries, a native Z3 API for
-Linux is bundled with Leon and should work out of the box
-(although having an external Z3 binary is a good idea in any
-case). For other platforms you will have to recompile the
-native Z3 communication layer yourself; see the section
-below.
-
-As of now the default solver is the native Z3 API, you will
-have to explicitly specify another solver if this native
-layer is not available to you, e.g., by giving the option
-``--solvers=smt-cvc4`` to use CVC4. Check the ``--solvers``
-option in :ref:`cmdlineoptions`.
-
-In addition to SMT solvers, it is possible to automatically
-invoke the Isabelle proof assistant on the proof obligations
-that Leon generates. See :ref:`isabelle` for details.
-
-Building ScalaZ3 and Z3 API
----------------------------
-
-The main reason for using the Z3 API is that it is currently
-faster when there are many calls to the solver, as in the
-case of synthesis and repair.
-
-To build the `ScalaZ3 <https://github.com/psuter/ScalaZ3/>`_
-on Linux, you should follow the instructions given in the
-ScalaZ3 project. The ScalaZ3 is a Scala wrapper on the Z3
-native library from Microsoft. It is used in Leon to make
-native call to Z3. The generated .jar from ScalaZ3 will be
-dependent on your own z3 native library, which you can
-obtain from http://z3.codeplex.com/ . However, the
-ScalaZ3 repository comes with 32 and 64 bits version for
-Linux and you should probably use those ones to make sure
-the version is compatible. You can install the Z3 native
-library in some standard system library path such as
-``/usr/lib``. You need to install the ``scalaz3.jar`` file in
-the "unmanaged" directory. The build system is configured to
-use any jar file in the "unmanaged" directory. Finally be
-aware that the Z3 library will come with its own set of
-dependencies, in particular you will need to have GMP. You
-will probably have to fight with a few errors before
-everything can finally work together.
-
-An analogous process has been reported to be relatively
-straightforward on OS-X and also possible on Windows.
-
-Running Tests
--------------
-
-Leon comes with a test suite. Consider running the following commands to
-invoke different test suites:
-
- $ sbt test
- $ sbt integration:test
- $ sbt regression:test
-
-Building Leon Documentation
----------------------------
-
-To build this documentation locally, you will need Sphinx (
-http://sphinx-doc.org/ ), a restructured text toolkit that
-was originally developed to support Python documentation.
-
-After installing sphinx, run ``sbt previewSite``. This will generate the documentation and open a browser.
-
-The documentation resides in the ``src/sphinx/`` directory and can also be built without ``sbt``
-using the provided ``Makefile``. To do this, in a Linux shell go to the directory ``src/sphinx/``,
-type ``make html``, and open in your web browser the generated top-level local HTML file, by default stored in
-``src/sphinx/_build/html/index.html``. Also, you can open the ``*.rst`` documentation files in a text editor, since
-they are human readable in their source form.
-
-Using Leon in Eclipse
----------------------
-
-You first need to tell sbt to globally include the Eclipse plugin in its known plugins.
-To do so type
-
-.. code-block:: bash
-
- $ echo "addSbtPlugin(\"com.typesafe.sbteclipse\" % \"sbteclipse-plugin\" % \"2.4.0\")" >> ~/.sbt/0.13/plugins/plugins.sbt
-
-In your Leon home folder, type: ```sbt clean compile eclipse```
-
-This should create all the necessary metadata to load Leon as a project in Eclipse.
-
-You should now be able to `import the project <http://help.eclipse.org/juno/index.jsp?topic=%2Forg.eclipse.platform.doc.user%2Ftasks%2Ftasks-importproject.htm>`_ into your Eclipse workspace. Don't forget to also import dependencies (the bonsai and scalaSmtlib projects, found somewhere in your ~/.sbt directory).
-
-For each run configuration in Eclipse, you have to set the
-``ECLIPSE_HOME`` environment variable to point to the home
-directory of your Eclipse installation. To do so, go to
-
-Run -> Run Configuration
-
-and then, after picking the configuration you want to run,
-set the variable in the Environment tab.
-
-If you want to use ScalaTest from within Eclipse, download the ScalaTest plugin. For instructions,
-see `Using ScalaTest with Eclise <http://www.scalatest.org/user_guide/using_scalatest_with_eclipse>`_.
-Do NOT declare your test packages as nested packages in
-separate lines, because ScalaTest will not see them for some
-reason. E.g. don't write
-
-.. code-block:: scala
-
- package leon
- package test
- package myTestPackage
-
-but instead
-
-.. code-block:: scala
-
- package leon.test.myTestPackage
-
diff --git a/src/sphinx/intro.rst b/src/sphinx/intro.rst
deleted file mode 100644
index c28c87c660a991ef543742e0ee8749ea1f4dcc68..0000000000000000000000000000000000000000
--- a/src/sphinx/intro.rst
+++ /dev/null
@@ -1,215 +0,0 @@
-Introduction
-============
-
-The Leon system aims to help developers build verified Scala software.
-It encourages using a small set of core Scala features, but provides
-unique automation functionality. In particular, Leon can
-
-* verify statically that your program confirms to a given
- specification and that it cannot crash at run-time
-
-* repair a program for you to ensure that the above holds
-
-* automatically execute and synthesize working functions
- from partial input/output specifications and test cases.
-
-Leon and Scala
---------------
-
-Leon attempts to strike a delicate balance between the convenience
-of use on the one hand and the simplicity of reasoning
-on the other hand.
-Leon primarily supports programs written in :ref:`Pure Scala <purescala>`, a purely
-functional subset of Scala.
-This fragment is at the core of
-the functional programming paradigm and lies at the intersection
-of functional languages such as Scala, Haskell, ML, and fragments present in interactive theorem provers such as Isabelle and Coq. Thus,
-if you do not already know Scala, learning the Leon subset should
-be easier as it is a smaller language.
-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.
-Leon's algorithms can map this fragment into the first-order language
-of SMT (satisfiability modulo theory) solvers, enabling
-efficient automated reasoning. Moreover, thanks to the use of
-``scalac`` front end, Leon supports implicits and ``for``
-comprehensions (which also serve as a syntax for monads in Scala).
-Leon also comes with a simple library of useful data types, which are designed
-to work well with automated reasoning and Leon's language fragment.
-
-In addition to this pure fragment, Leon supports the
-:ref:`XLang <xlang>` extension, which enables Leon to work
-on a richer subset of Scala, including imperative features.
-Features introduced by :ref:`XLang <xlang>` are handled by
-translation into Pure Scala concepts. They are often more
-than just syntactic sugar, because some of them require
-significant modification of the original program, such as
-introducing additional parameters to a set of functions. As
-an intended aspect of its current design, Leon's language
-currently does not provide a default encoding of
-e.g. concurrency with a shared mutable heap, though it might
-support more manageable forms of concurrency in the future.
-For practical reasons, Leon programs can also call out into
-general Scala code, which needs to be used with care as it
-is a form of "foreign function interface" into the general
-world of Scala.
-
-If you would like to use Leon now, check the :ref:`Getting Started <gettingstarted>`
-section and try our :ref:`Tutorial <tutorial>`.
-To learn more about the functionality that Leon provides, read on below.
-
-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 satisfying 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 occurring in the external
- theorem prover.
-
-Leon will also verify for each call site that the precondition of the invoked
-function cannot be violated.
-
-Leon supports verification of a significant part of the Scala language, described in the
-sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`.
-
-
-
-
-Program Synthesis
------------------
-
-As seen with verification, specifications provide an alternative and more
-descriptive way of characterizing the behavior of a function.
-Leon defines ways to use specifications instead of an actual implementation
-within your programs:
-
-* a ``choose`` construct that describes explicitly a value with a
- specification. For instance, one could synthesize a function inserting into a
- sorted list by:
-
-.. code-block:: scala
-
- def insert1(in: List, v: BigInt) = {
- require(isSorted(in1))
- choose { (out: List) =>
- (content(out) == content(in1) ++ Set(v)) && isSorted(out)
- }
- }
-
-* a hole (``???``) that can be placed anywhere in a specified function. Leon
- will fill it with values such that the overall specification is satisfied.
- This construct is especially useful when only a small part of the function
- is missing.
-
-.. code-block:: scala
-
- def insert2(in: List, v: BigInt) = {
- require(isSorted(in1))
- in match {
- case Cons(h, t) =>
- if (h < v) {
- Cons(h, in)
- } else if (h == v) {
- in
- } else {
- ???[List]
- }
- case Nil =>
- Nil
- }
- } ensuring { out =>
- (content(out) == content(in1) ++ Set(v)) && isSorted(out)
- }
-
-
-Given such programs, Leon can:
-
- 1) Execute them: when the evaluator encounters a ``choose`` construct, it
- solves the constraint at runtime by invoking an SMT solver. This allows some
- form of constraint solving programming.
-
- 2) Attempt to translate specifications to a traditional implementation by
- applying program synthesis. In our case, Leon will automatically synthesize
- the hole in ``insert2`` with ``Cons(h, insert2(v, t))``. This automated
- translation is described in further details in the section on :ref:`synthesis
- <Synthesis>`.
-
-
-
-Program Repair
---------------
-
-Leon can repair buggy :ref:`Pure Scala <purescala>` programs.
-Given a specification and an erroneous implementation, Leon will
-localize the cause of the bug and provide an alternative solution.
-An example:
-
-.. code-block:: scala
-
- def moddiv(a: Int, b: Int): (Int, Int) = {
- require(a >= 0 && b > 0);
- if (b > a) {
- (1, 0) // fixme: should be (a, 0)
- } else {
- val (r1, r2) = moddiv(a-b, b)
- (r1, r2+1)
- }
- } ensuring {
- res => b*res._2 + res._1 == a
- }
-
-Invoking ``leon --repair --functions=moddiv`` will yield: ::
-
- ...
- [ Info ] Found trusted solution!
- [ Info ] ============================== Repair successful: ==============================
- [ Info ] --------------------------------- Solution 1: ---------------------------------
- [ Info ] (a, 0)
- [ Info ] ================================= In context: =================================
- [ Info ] --------------------------------- Solution 1: ---------------------------------
- [ Info ] def moddiv(a : Int, b : Int): (Int, Int) = {
- require(a >= 0 && b > 0)
- if (b > a) {
- (a, 0)
- } else {
- val (r1, r2) = moddiv(a - b, b)
- (r1, (r2 + 1))
- }
- } ensuring {
- (res : (Int, Int)) => (b * res._2 + res._1 == a)
- }
-
-Repair assumes a small number of localized errors.
-It first invokes a test-based fault localization algorithm,
-and then a special synthesis procedure, which is partially guided
-by the original erroneous implementation. For more information,
-see the section on :ref:`Repair <repair>`.
-
diff --git a/src/sphinx/invinference.rst b/src/sphinx/invinference.rst
deleted file mode 100644
index 4c79f79c7d8eacd999f55d0f198aa7b45a8be01a..0000000000000000000000000000000000000000
--- a/src/sphinx/invinference.rst
+++ /dev/null
@@ -1,13 +0,0 @@
-.. _infinference:
-
-Invariant Inference
-===================
-
-The command line options relevant for invariant inference are
-listed under Invariant Inference section of :ref:`cmdlineoptions`.
-
-
-For examples, check out the directory ``testcases/orb-testcases/``.
-
-For any questions, please consult Ravi and check the paper
-`Symbolic resource bound inference for functional programs <http://lara.epfl.ch/~kuncak/papers/MadhavanKuncak14SymbolicResourceBoundInferenceFunctionalPrograms.pdf>`_, by *Ravichandhran Madhavan* and *Viktor Kuncak*. Computer Aided Verification (CAV), 2014.
diff --git a/src/sphinx/isabelle.rst b/src/sphinx/isabelle.rst
deleted file mode 100644
index a375ccb4302926d839b2b8015b7af09d34b866cf..0000000000000000000000000000000000000000
--- a/src/sphinx/isabelle.rst
+++ /dev/null
@@ -1,236 +0,0 @@
-.. _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 don't have to obtain a copy of Isabelle. Leon is able to download and
-install Isabelle itself. The installation happens in the appropriate folder for
-your operating system, e.g. ``%APPDATA%`` under Windows or ``$HOME/.local``
-under Linux.
-
-
-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/library.rst b/src/sphinx/library.rst
deleted file mode 100644
index 5cbb60c2dfc91266a52e0a273ae0647162832a36..0000000000000000000000000000000000000000
--- a/src/sphinx/library.rst
+++ /dev/null
@@ -1,315 +0,0 @@
-.. _library:
-
-Leon Library
-============
-
-Leon defines its own library with some core data types and
-operations on them, which work with the fragment supported
-by Leon. One of the reasons for a separate library is to
-ensure that these operations can be correctly mapped to
-mathematical functions and relations inside of SMT solvers,
-largely defined by the SMT-LIB standard (see
-http://www.smt-lib.org/). Thus for some data types, such as
-``BigInt``, Leon provides a dedicated mapping to support reasoning.
-(If you are a fan
-of growing the language only through libraries, keep in mind that
-growing operations together with the ability to reason about them
-is what the development of mathematical theories is all about, and
-is a process slower than putting together
-libraries of unverified code--efficient automation of reasoning about a
-single decidable theory generally results in multiple research papers.)
-For other operations (e.g., `List[T]`), the library
-is much like Leon user-defined code, but specifies some
-useful preconditions and postconditions of the operations, thus
-providing reasoning abilities using mechanisms entirely available
-to the user.
-
-To use Leon's libraries, you need to use the appropriate
-`import` directive at the top of Leon's compilation units.
-Here is a quick summary of what to import.
-For the most up-to-date version of the library,
-please consult the ``library/`` directory in your Leon
-distribution.
-
-+--------------------------------+----------------------------------------------------+
-| Package to import | What it gives access to |
-+================================+====================================================+
-| `leon.annotation` | Leon annotations, e.g. @induct |
-+--------------------------------+----------------------------------------------------+
-| `leon.lang` | `Map`, `Set`, `holds`, `passes`, `invariant` |
-+--------------------------------+----------------------------------------------------+
-| `leon.collection._` | List[T] and subclasses, Option[T] and subclasses |
-+--------------------------------+----------------------------------------------------+
-| `leon.lang.string` | String |
-+--------------------------------+----------------------------------------------------+
-| `leon.lang.xlang` | epsilon |
-+--------------------------------+----------------------------------------------------+
-| `leon.lang.synthesis` | choose, ???, ?, ?! |
-+--------------------------------+----------------------------------------------------+
-
-To learn more, we encourage you to
-look in the `library/` subdirectory of Leon distribution.
-
-Annotations
------------
-
-Leon provides some special annotations in the package ``leon.annotation``,
-which instruct Leon to handle some functions or objects in a specialized way.
-
-+-------------------+---------------------------------------------------+
-| Annotation | Meaning |
-+===================+===================================================+
-| ``@library`` | Treat this object/function as library, don't try |
-| | to verify its specification. Can be overriden by |
-| | including a function name in the ``--functions`` |
-| | command line option. |
-+-------------------+---------------------------------------------------+
-| ``@induct`` | Use the inductive tactic when generating |
-| | verification conditions. |
-+-------------------+---------------------------------------------------+
-| ``@ignore`` | Ignore this definition when extracting Leon trees.|
-| | This annotation is useful to define functions |
-| | that are not in Leon's language but will be |
-| | hard-coded into specialized trees, or to include |
-| | code written in full Scala which is not verifiable|
-| | by Leon. |
-+-------------------+---------------------------------------------------+
-| ``@inline`` | Inline this function. Leon will refuse to inline |
-| | (mutually) recursive functions. |
-+-------------------+---------------------------------------------------+
-
-List[T]
--------
-
-As there is no special support for Lists in SMT solvers, Leon Lists are encoded
-as an ordinary algebraic data type:
-
-.. code-block:: scala
-
- sealed abstract class List[T]
- case class Cons[T](h: T, t: List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
-
-List API
-********
-
-Leon Lists support a rich and strongly specified API.
-
-+---------------------------------------------------+---------------------------------------------------+
-| Method signature for ``List[T]`` | Short description |
-+===================================================+===================================================+
-| ``size: BigInt`` | Number of elements in this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``content: Set[T]`` | The set of elements in this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``contains(v: T): Boolean`` | Returns true if this List contains ``v``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``++(that: List[T]): List[T]`` | Append this List with ``that``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``head: T`` | Returns the head of this List. Can only be called |
-| | on a nonempty List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``tail: List[T]`` | Returns the tail of this List. Can only be called |
-| | on a nonempty List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``apply(index: BigInt): T`` | Return the element in index ``index`` in this |
-| | List (0-indexed). |
-+---------------------------------------------------+---------------------------------------------------+
-| ``::(t:T): List[T]`` | Prepend an element to this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``:+(t:T): List[T]`` | Append an element to this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``reverse: List[T]`` | The reverse of this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``take(i: BigInt): List[T]`` | Take the first ``i`` elements of this List, or |
-| | the whole List if it has less than ``i`` elements.|
-+---------------------------------------------------+---------------------------------------------------+
-| ``drop(i: BigInt): List[T]`` | This List without the first ``i`` elements, |
-| | or the Nil() if this List has less than ``i`` |
-| | elements. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``slice(from: BigInt, to: BigInt): List[T]`` | Take a sublist of this List, from index ``from`` |
-| | to index ``to``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``replace(from: T, to: T): List[T]`` | Replace all occurrences of ``from`` in this List |
-| | with ``to``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``chunks(s: BigInt): List[List[T]]`` | |
-+---------------------------------------------------+---------------------------------------------------+
-| ``zip[B](that: List[B]): List[(T, B)]`` | Zip this list with ``that``. In case the Lists |
-| | do not have equal size, take a prefix of the |
-| | longer. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``-(e: T): List[T]`` | Remove all occurrences of ``e`` from this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``--(that: List[T]): List[T]`` | Remove all occurrences of any element in ``that`` |
-| | from this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``&(that: List[T]): List[T]`` | A list of all elements that occur both in |
-| | ``that`` and this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``pad(s: BigInt, e: T): List[T]`` | Add ``s`` instances of ``e`` at the end of this |
-| | List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``find(e: T): Option[BigInt]`` | Look for the element ``e`` in this List, and |
-| | optionally return its index if it is found. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``init: List[T]`` | Return this List except the last element. |
-| | Can only be called on nonempty Lists. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``last: T`` | Return the last element of this List. |
-| | Can only be called on nonempty Lists. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``lastOption: Option[T]`` | Optionally return the last element of this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``headOption: Option[T]`` | Optionally return the first element of this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``unique: List[T]`` | Return this List without duplicates. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``splitAt(e: T): List[List[T]]`` | Split this List to chunks separated by an |
-| | occurrence of ``e``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``split(seps: List[T]): List[List[T]]`` | Split this List in chunks separated by an |
-| | occurrence of any element in ``seps``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``count(e: T): BigInt`` | Count the occurrences of ``e`` in this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``evenSplit: (List[T], List[T])`` | Split this List in two halves. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``insertAt(pos: BigInt, l: List[T]): List[T]`` | Insert an element after index ``pos`` in this |
-| | List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``replaceAt(pos: BigInt, l: List[T]): List[T]`` | Replace the ``l.size`` elements after index |
-| | ``pos``, or all elements after index ``pos`` |
-| | if there are not enough elements, |
-| | with the elements in ``l``. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``rotate(s: BigInt): List[T]`` | Rotate this list by ``s`` positions. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``isEmpty: Boolean`` | Returns whether this List is empty. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``map[R](f: T => R): List[R]`` | Builds a new List by applying a predicate ``f`` |
-| | to all elements of this list. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``foldLeft[R](z: R)(f: (R,T) => R): R`` | Applies the binary operator ``f`` to a start value|
-| | ``z`` and all elements of this List, going left |
-| | to right. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``foldRight[R](f: (T,R) => R)(z: R): R`` | Applies a binary operator ``f`` to all elements of|
-| | this list and a start value ``z``, going right to |
-| | left. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``scanLeft[R](z: R)(f: (R,T) => R): List[R]`` | Produces a List containing cumulative results |
-| | of applying the operator ``f`` going left to |
-| | right. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``scanRight[R](f: (T,R) => R)(z: R): List[R]`` | Produces a List containing cumulative results |
-| | of applying the operator ``f`` going right to |
-| | left. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``flatMap[R](f: T => List[R]): List[R]`` | Builds a new List by applying a function ``f`` |
-| | to all elements of this list and using the |
-| | elements of the resulting Lists. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``filter(p: T => Boolean): List[T]`` | Selects all elements of this List |
-| | which satisfy the predicate ``p`` |
-+---------------------------------------------------+---------------------------------------------------+
-| ``forall(p: T => Boolean): Boolean`` | Tests whether predicate ``p`` holds |
-| | for all elements of this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``exists(p: T => Boolean): Boolean`` | Tests whether predicate ``p`` holds for some of |
-| | the elements of this List. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``find(p: T => Boolean): Option[T]`` | Finds the first element of this List satisfying |
-| | predicate ``p``, if any. |
-+---------------------------------------------------+---------------------------------------------------+
-| ``takeWhile(p: T => Boolean): List[T]`` | Takes longest prefix of elements that satisfy |
-| | predicate ``p`` |
-+---------------------------------------------------+---------------------------------------------------+
-
-List.apply(e: T*)
-*****************
-
-It is possible to create Lists with varargs like in regular Scala,
-for example ``List(1,2,3)`` or ``List()``. This expression will be
-desugared into a series of applications of ``Cons``.
-
-Additional operations on Lists
-******************************
-
-The object ``ListOps`` offers this additional operations:
-
-+--------------------------------------------------------+---------------------------------------------------+
-| Function signature | Short description |
-+========================================================+===================================================+
-| ``flatten[T](ls: List[List[T]]): List[T]`` | Converts the List of Lists ``ls`` into a List |
-| | formed by the elements of these Lists. |
-+--------------------------------------------------------+---------------------------------------------------+
-| ``isSorted(ls: List[BigInt]): Boolean`` | Returns whether this list of mathematical integers|
-| | is sorted in ascending order. |
-+--------------------------------------------------------+---------------------------------------------------+
-| ``sorted(ls: List[BigInt]): List[BigInt]`` | Sorts this list of mathematical integers |
-| | is sorted in ascending order. |
-+--------------------------------------------------------+---------------------------------------------------+
-| ``insSort(ls: List[BigInt], v: BigInt): List[BigInt]`` | Sorts this list of mathematical integers |
-| | is sorted in ascending order using insertion sort.|
-+--------------------------------------------------------+---------------------------------------------------+
-
-Theorems on Lists
-*****************
-
-The following theorems on Lists have been proven by Leon and are included
-in the object ``ListSpecs``:
-
-+---------------------------------------------------------------+--------------------------------------------------------+
-| Theorem signature | Proven Claim |
-+===============================================================+========================================================+
-| ``snocIndex[T](l : List[T], t : T, i : BigInt)`` | ``(l :+ t).apply(i) == (if (i < l.size) l(i) else t)`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``reverseIndex[T](l : List[T], i : BigInt)`` | ``l.reverse.apply(i) == l.apply(l.size - 1 - i)`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``appendIndex[T](l1 : List[T], l2 : List[T], i : BigInt)`` | ``(l1 ++ l2).apply(i) ==`` |
-| | ``(if (i < l1.size) l1(i) else l2(i - l1.size))`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``appendAssoc[T](l1 : List[T], l2 : List[T], l3 : List[T])`` | ``((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3))`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``snocIsAppend[T](l : List[T], t : T)`` | ``(l :+ t) == l ++ Cons[T](t, Nil())`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``snocAfterAppend[T](l1 : List[T], l2 : List[T], t : T)`` | ``(l1 ++ l2) :+ t == (l1 ++ (l2 :+ t))`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``snocReverse[T](l : List[T], t : T)`` | ``(l :+ t).reverse == Cons(t, l.reverse)`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``reverseReverse[T](l : List[T])`` | ``l.reverse.reverse == l`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-| ``scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B)`` | ``l.scanRight(f)(z).head == l.foldRight(f)(z)`` |
-+---------------------------------------------------------------+--------------------------------------------------------+
-
-Set[T], Map[T]
---------------
-
-Leon uses its own Sets and Maps, which are defined in the ``leon.lang`` package.
-However, these classes are are not implemented within Leon.
-Instead, they are parsed into specialized trees.
-Methods of these classes are mapped to specialized trees within SMT solvers.
-For code generation, we rely on Java Sets and Maps.
-
-The API of these classes is a subset of the Scala API and can be found
-in the :ref:`purescala` section.
-
-Additionally, the following functions for Sets are provided in the
-``leon.collection`` package:
-
-
-+-----------------------------------------------------------+-------------------------------------------+
-| Function signature | Short description |
-+===========================================================+===========================================+
-| ``setToList[A](set: Set[A]): List[A]`` | Transforms the Set ``set`` into a List. |
-+-----------------------------------------------------------+-------------------------------------------+
-| ``setForall[A](set: Set[A], p: A => Boolean): Boolean`` | Tests whether predicate ``p`` holds |
-| | for all elements of Set ``set``. |
-+-----------------------------------------------------------+-------------------------------------------+
-| ``setExists[A](set: Set[A], p: A => Boolean): Boolean`` | Tests whether predicate ``p`` holds |
-| | for all elements of Set ``set``. |
-+-----------------------------------------------------------+-------------------------------------------+
-
diff --git a/src/sphinx/limitations.rst b/src/sphinx/limitations.rst
deleted file mode 100644
index 8445a4145c7cb2778c74ff224b1f2517863608ac..0000000000000000000000000000000000000000
--- a/src/sphinx/limitations.rst
+++ /dev/null
@@ -1,41 +0,0 @@
-.. _limitations:
-
-Limitations of Verification
----------------------------
-
-A goal of Leon is to ensure that proven properties hold in
-all program executions so that, for example, verified programs
-do not crash and all of the preconditions and postconditions
-are true in all executions.
-For this to be the case, there needs
-to be a precise correspondence between runtime execution
-semantics and the semantics used in verification, including
-the SMT solvers invoked.
-
-Below we document several cases where we are aware that the
-discrepancy exists and provide suggested workarounds.
-
-Out of Memory Errors
-^^^^^^^^^^^^^^^^^^^^
-
-By default Leon assumes that unbounded data types can
-be arbitrarily large and that all well-founded recursive
-functions have enough stack space to finish their computation.
-Thus a verified program may crash at run-time due to:
-
- * stack overflow
- * heap overflow
-
-Algebraic data types are assumed to be arbitrarily large.
-In any given execution, there will be actual bounds on the
-total available memory, so the program could crash with out
-of memory error when trying to allocate another value of
-algebraic data type.
-
-For a safety critical application you may wish to resort to
-tail-recursive programs only, and also write preconditions
-and postconditions that enforce a bound on the maximum size
-of the data structures that your application
-manipulates. For this purpose, you can define size functions
-that return `BigInt` data types.
-
diff --git a/src/sphinx/neon.rst b/src/sphinx/neon.rst
deleted file mode 100644
index f830531ce911d4be9d50c33c2c29cd9da8954f98..0000000000000000000000000000000000000000
--- a/src/sphinx/neon.rst
+++ /dev/null
@@ -1,1004 +0,0 @@
-.. _neon:
-
-Proving Theorems
-================
-
-Verifying the contract of a function is really proving a mathematical
-theorem. Leon can be seen as a (mostly) automated theorem prover. It is
-automated in the sense that once the property stated, Leon will proceed with searching
-for a proof without any user interaction. In practice however, many theorems will be fairly
-difficult to prove, and it is possible for the user to provide hints to Leon.
-
-Hints typically take the form of simpler properties that combine in order to prove
-more complicated ones. In the remaining subsections we provide code patterns and introduce
-simple domain-specific language operators that can help in constructing complex Leon proofs.
-
-A practical introduction to proofs
-----------------------------------
-
-When writing logical propositions such as preconditions or
-postconditions in Leon, one is basically writing Boolean
-predicates. They can be as simple as testing whether a list is empty
-or not, to more complex combinations of properties. Lemmas or
-theorems are simply logical tautologies, that is, propositions that
-always hold. They can be expressed using Boolean-valued methods that
-return ``true`` for all their inputs.
-
-To make this more concrete, let's take a simple lemma as an
-example [#example-dir]_. Here we want to prove that the append operation (``++``) on
-lists preserves the content of the two lists being concatenated. This
-proposition is relatively straightforward and Leon is able to verify
-that it always holds.
-
-.. code-block:: scala
-
- import leon.collection._ // for List
- import leon.lang._ // for holds
-
- object Example {
- def appendContent[A](l1: List[A], l2: List[A]): Boolean = {
- l1.content ++ l2.content == (l1 ++ l2).content
- }.holds
- }
-
-Here we wrote ``.holds`` which is a method implicitly available on ``Boolean``
-that ensure the returned value is ``true``. It is equivalent to writing
-``ensuring { res => res }``.
-
-Now let's look at another example that looks trivial but for which Leon
-actually needs some help with the proof: we want to prove that adding ``Nil``
-at the end of a list has no effect.
-
-.. code-block:: scala
-
- import leon.collection._ // for List
- import leon.lang._ // for holds
-
- object Example {
- def rightUnitAppend[T](l1: List[T]): Boolean = {
- l1 ++ Nil() == l1
- }.holds
- }
-
-If you try to verify this last example you'll face a delicate
-situation: Leon runs indeterminately until it is either killed or
-times out. But why does this happen? The proposition doesn't seems
-more complicated than ``appendContent``. Perhaps even more
-surprisingly, Leon *is* able to verify the following:
-
-.. code-block:: scala
-
- def leftUnitAppend[T](l1: List[T]): Boolean = {
- Nil() ++ l1 == l1
- }.holds
-
-How is this possible? The two propositions are completely symmetric!
-The problem is that Leon doesn't know anything about lists, a priori.
-It can only reason about lists thanks to their definition in terms of
-the case classes ``Cons`` and ``Nil`` and associated methods such as
-``++``. In particular, Leon doesn't know that ``Nil`` represents the
-empty list, and hence that appending it to some other list is a no-op.
-What then, is the difference between the two examples above? To
-answer this question, we need to have a look at the definition of the
-``++`` method:
-
-.. code-block:: scala
-
- def ++(that: List[T]): List[T] = (this match {
- case Nil() => that
- case Cons(x, xs) => Cons(x, xs ++ that)
- }) ensuring { res => /* ... */ }
-
-Note that the implementation of ``++`` is recursive in its first
-argument ``this`` but *not* in its second argument ``that``. This is
-why Leon was able to verify ``leftUnitAppend`` easily: it is true *by
-definition*, i.e. ``Nil() ++ l1`` is actually defined to be ``l1``.
-What about the symmetric case? How is ``l1 ++ Nil()`` defined? Well,
-it depends on whether ``l1`` is the empty list or not. So in order to
-prove ``rightUnitAppend``, we need to proceed by case analysis. The
-resulting proof has a recursive (i.e. inductive) structure reminiscent
-of the definition of ``++``:
-
-.. code-block:: scala
-
- import leon.collection._ // for List
- import leon.lang._ // for holds
- import leon.proof._ // for because
-
- object Example {
- def rightUnitAppend[T](l1: List[T]): Boolean = {
- (l1 ++ Nil() == l1) because {
- l1 match {
- case Nil() => true
- case Cons(x, xs) => rightUnitAppend(xs)
- }
- }
- }.holds
- }
-
-With this new implementation of the ``rightUnitAppend`` lemma, Leon is capable
-of verifying that it holds. If you look closely at it, you can distinguish three
-parts:
-
-1. the claim we want to prove ``l1 ++ Nil() == l1``;
-2. ``because``, which is just some syntactic sugar for conjunction -- remember,
- every proposition is a Boolean formula;
-3. and a recursion on ``l1`` that serves as a hint for Leon to perform
- induction.
-
-The recursion is based here on pattern matching, which Leon will also check for
-exhaustiveness. It has essentially the same structure as
-the implementation of ``++``: the base case is when ``l1`` is the empty list
-and the inductive case is performed on ``Cons`` objects.
-
-
-Techniques for proving non-trivial propositions
------------------------------------------------
-
-In the previous section we saw that "proof hints" can improve the odds
-of Leon successfully verifying a given proposition. In this section
-we will have a closer look at what constitutes such a proof and
-discuss a few techniques for writing them.
-
-As mentioned earlier, propositions are represented by Boolean
-expressions in Leon. But how are proofs represented? They are just
-Boolean expressions as well [#props-not-types]_. The difference
-between propositions and proofs is not their representation, but how
-they are used by Leon. Intuitively, a proof ``p: Boolean`` for a
-proposition ``x: Boolean`` is an expression such that
-
- 1. Leon is able to verify ``p``, and
- 2. Leon is able to verify that ``p`` implies ``x``.
-
-This is what we mean when we say that proofs are "hints". Typically,
-a proof ``p`` of a proposition ``x`` is a more complex-looking but
-equivalent version of ``x``, i.e. an expression such that ``p == x``.
-This might seem a bit counter-intuitive: why should it be easier for
-Leon to verify an equivalent but more complex expression? The answer
-is that the more complex version may consist of sub-expressions that
-more closely resemble the definitions of functions used in ``x``. We
-have already seen an example of this principle in the previous
-section: let's have another look at the proof of ``rightUnitAppend``:
-
-.. code-block:: scala
-
- def rightUnitAppend[T](l1: List[T]): Boolean = {
- val x = l1 ++ Nil() == l1
- val p = l1 match {
- case Nil() => true
- case Cons(x, xs) => rightUnitAppend(xs)
- }
- x because p
- }.holds
-
-Here, we have rewritten the example to make the distinction between
-the proposition ``x`` and its proof ``p`` more explicit. It's easy to
-check that indeed ``x == p``, and hence the overall result of
-``rightUnitAppend`` is equivalent to ``x`` (recall that ``because`` is
-just an alias of ``&&``, so ``(x because p) == (x && x) == x``).
-However, the proof term ``p`` closely resembles the definition of
-``++`` and its sub-expressions are easier to verify for Leon than
-``x`` itself. The only non-trivial expression is the recursive call
-to ``rightUnitAppend(xs)``, which serves as the inductive hypothesis.
-We will discuss induction in more detail in Section
-":ref:`induction`".
-
-
-Divide and Conquer
-******************
-
-Before we delve into the details of particular proof techniques, it is
-worth revisiting a guiding principle for writing proofs -- whether it
-be in Leon, by hand, or using some other form of mechanized proof
-checker -- namely to *modularize* proofs, i.e. to split the proofs of
-complex propositions into manageable *sub-goals*. This can be
-achieved in various ways.
-
- * Use *helper lemmas* -- these are propositions that are lemmas on
- their own, i.e. they state and prove simple but self-contained
- propositions that can be reused elsewhere. As such, they play a
- role akin to helper methods in normal programming, and indeed, are
- implemented in the same way, except that they carry a ``.holds``
- suffix.
-
- * Use *case analysis* to split complex propositions into simpler
- sub-cases. This is especially helpful in the presence of
- recursion, where it leads to inductive proofs (see Section
- ":ref:`induction`").
-
- * Use *relational reasoning* to split complex relationships into
- conjunctions of elementary ones. This often requires one to make
- use of relational properties such as transitivity (e.g. to break a
- single equation ``a == b`` into a chain of equations ``a == x1 &&
- x1 == x2 && ... && xN == b``), symmetry (e.g. to use a previously
- proven inequality ``a <= b`` where ``b >= a`` is expected),
- anti-symmetry (to unify variables), and so on (see Section
- ":ref:`rel-reasoning`").
-
- * Separate specification form implementation. It is sometimes easier
- to prove the fact that a given function fulfills its specification
- as a separate lemma (although the proof techniques are roughly the
- same, see Section ":ref:`post-cond`").
-
- * Generalize (or specialize) propositions. Sometimes, propositions
- are more easily proved in a stronger (or weaker) form and
- subsequently instantiated (or combined with other propositions) to
- yield a proof of the original proposition.
-
-While it is good practice to factor common propositions into helper
-lemmas, one sometimes wants to verify simple, specific sub-goals in a
-proof without going through the trouble of introducing an additional
-method. This is especially true while one is exploring the branches
-of a case analysis or wants to quickly check whether Leon is able to
-prove a seemingly trivial statement automatically (we will see
-examples of such situations in the coming sections). For such cases,
-one can use the ``check`` function from ``leon.proof``. The ``check``
-function behaves as the identity function on Booleans but additionally
-assumes its argument in its precondition. As a result, Leon will
-check that ``x`` holds while verifying the call to ``check(x)``.
-For example, when verifying the following function:
-
-.. code-block:: scala
-
- import leon.proof.check
-
- def foo(x: BigInt): Boolean = {
- check(x >= 0 || x < 0) && check(x + 0 == 0)
- }
-
-Leon will check (separately) that ``x >= 0 || x < 0`` and ``x + 0 ==
-0`` hold for all ``x``, even though the function ``foo`` does not
-specify any pre or postconditions, and report a counter example for
-the second case::
-
- [ Info ] - Now considering 'precond. (call check(x >= 0 || x < 0))' VC for foo @40:5...
- [ Info ] => VALID
- [ Info ] - Now considering 'precond. (call check(x + 0 == 0))' VC for foo @40:31...
- [ Error ] => INVALID
- [ Error ] Found counter-example:
- [ Error ] x -> 1
-
-This is especially helpful when "debugging" proofs.
-
-
-.. _induction:
-
-Induction
-*********
-
-The vast majority of functional programs are written as functions over
-:ref:`adts` (ADTs), and consequently, Leon comes with some special
-support for verifying properties of ADTs. Among other things, Leon
-provides an annotation ``@induct``, which can be used to automatically
-prove postconditions of recursive functions defined on ADTs by way of
-*structural induction*. We have already seen an example of such an
-inductive property, namely ``rightUnitAppend``. In fact, using
-``@induct``, Leon is able to prove ``rightUnitAppend`` directly:
-
-.. code-block:: scala
-
- import leon.annotation._ // for @induct
-
- @induct
- def rightUnitAppend[T](l1: List[T]): Boolean = {
- l1 ++ Nil() == l1
- }.holds
-
-This is possible because the inductive step follows (more or less)
-directly from the inductive hypothesis and Leon can verify the base
-case automatically. However, Leon may fail to verify more complex
-functions with non-trivial base cases or inductive steps. In such
-cases, one may still try to provide proof hints by performing *manual
-case analysis*. Consider the following lemma about list reversal:
-
-.. code-block:: scala
-
- import leon.collection._ // for List
- import leon.lang._ // for holds
-
- object Example {
- def reverseReverse[T](l: List[T]): Boolean = {
- l.reverse.reverse == l
- }.holds
- }
-
-Leon is unable to verify ``reverseReverse`` even using ``@induct``.
-So let's try and prove the lemma using manual case analysis. We start
-by adding an "unrolled" version of the proposition and inserting calls
-to ``check`` in each branch of the resulting pattern match:
-
-.. code-block:: scala
-
- def reverseReverse[T](l: List[T]): Boolean = {
- l.reverse.reverse == l because {
- l match {
- case Nil() => check { Nil[T]().reverse.reverse == Nil[T]() }
- case Cons(x, xs) => check { (x :: xs).reverse.reverse == (x :: xs) }
- }
- }
- }.holds
-
-Clearly, the two versions of the lemma are equivalent: all we did was
-expand the proposition using a pattern match and add some calls to
-``check`` (remember ``check`` acts as the identity function on its
-argument). Let's see what output Leon produces for the expanded
-version::
-
- [ Info ] - Now considering 'postcondition' VC for reverseReverse @615:5...
- [Warning ] => UNKNOWN
- [ Info ] - Now considering 'precond. (call check(List[T]().reverse().reverse() ...)' VC for reverseReverse @617:28...
- [ Info ] => VALID
- [ Info ] - Now considering 'precond. (call check({val x$27 = l.h; ...)' VC for reverseReverse @618:28...
- [Warning ] => UNKNOWN
- [ Info ] - Now considering 'match exhaustiveness' VC for reverseReverse @616:7...
- [ Info ] => VALID
-
-As expected, Leon failed to verify the expanded version. However, we
-get some additional information due to the extra pattern match and the
-calls to ``check``. In particular, Leon tells us that the match is
-exhaustive, which means we covered all the cases in our case analysis
--- that's certainly a good start. Leon was also able to automatically
-verify the base case, so we can either leave the call to ``check`` as
-is, or replace it by ``trivial``. Unfortunately, Leon wasn't able to
-verify the inductive step, something is missing. Let's try to
-manually reduce the inductive case and see where we get.
-
-.. code-block:: scala
-
- def reverseReverse[T](l: List[T]): Boolean = {
- l.reverse.reverse == l because {
- l match {
- case Nil() => trivial
- case Cons(x, xs) => check { (xs.reverse :+ x).reverse == (x :: xs) }
- }
- }
- }.holds
-
-And now we're stuck. We can't apply the inductive hypothesis here,
-nor can we reduce the inductive case further, unless we perform
-case analysis on ``xs``, which would grow the term further without
-changing its shape. To make any headway, we need to use an additional
-property of ``reverse``, given by the following lemma (which Leon *is*
-able to prove using ``@induct``):
-
-.. code-block:: scala
-
- @induct
- def snocReverse[T](l: List[T], t: T): Boolean = {
- (l :+ t).reverse == t :: l.reverse
- }.holds
-
-The lemma states that appending an element ``t`` to a list ``l`` and
-reversing it is equivalent to first reversing ``l`` and then
-prepending ``t``. Using this lemma, we can write the proof of
-``reverseReverse`` as
-
-.. code-block:: scala
-
- def reverseReverse[T](l: List[T]): Boolean = {
- l.reverse.reverse == l because {
- l match {
- case Nil() => trivial
- case Cons(x, xs) => check {
- (xs.reverse :+ x).reverse == x :: xs.reverse.reverse &&
- x :: xs.reverse.reverse == (x :: xs) because
- snocReverse(xs.reverse, x) && reverseReverse(xs)
- }
- }
- }
- }.holds
-
-Leon is able to verify this version of the lemma. Note that Leon
-doesn't actually require us to include the two equations as they are
-equivalent to the applications ``snocReverse(xs.reverse, x)`` and
-``reverseReverse(xs)``. Similarly, the call to ``check`` is somewhat
-redundant now that Leon is able to verify the entire proof. We could
-thus "simplify" the above to
-
-.. code-block:: scala
-
- def reverseReverse[T](l: List[T]): Boolean = {
- l.reverse.reverse == l because {
- l match {
- case Nil() => trivial
- case Cons(x, xs) => snocReverse(xs.reverse, x) && reverseReverse(xs)
- }
- }
- }.holds
-
-However, the previous version is arguably more readable for a human
-being, and therefore preferable. In Section ":ref:`rel-reasoning`" we
-will see how readability can be improved even further through the use
-of a DSL for equational reasoning.
-
-So far, we have only considered structurally inductive proofs.
-However, Leon is also able to verify proofs using *natural induction*
--- the form of induction that is perhaps more familiar to most
-readers. Consider the following definition of the exponential
-function :math:`exp(x, y) = x^y` over integers:
-
-.. code-block:: scala
-
- def exp(x: BigInt, y: BigInt): BigInt = {
- require(y >= 0)
- if (x == 0) 0
- else if (y == 0) 1
- else x * exp(x, y - 1)
- }
-
-The function ``exp`` is again defined recursively, but this time using
-``if`` statements rather than pattern matching. Let's try and prove
-some properties of this function using natural induction. One such
-property is that for any pair of positive numbers :math:`x, y \geq 0`,
-the exponential :math:`x^y` is again a positive number.
-
-.. code-block:: scala
-
- def positive(x: BigInt, y: BigInt): Boolean = {
- require(y >= 0 && x >= 0)
- exp(x, y) >= 0
- }
-
-Since Leon doesn't know anything about exponentials, it isn't able to
-verify the lemma without hints. As with the previous example, we
-start writing our inductive proof by expanding the top-level ``if``
-statement in the definition of ``exp``.
-
-.. code-block:: scala
-
- def positive(x: BigInt, y: BigInt): Boolean = {
- require(y >= 0 && x >= 0)
- exp(x, y) >= 0 because {
- if (x == 0) check { exp(x, y) >= 0 } // <-- valid
- else if (y == 0) check { exp(x, y) >= 0 } // <-- valid
- else check { exp(x, y) >= 0 } // <-- unknown
- }
- }.holds
-
-Leon was able to verify the first two (base) cases, but not the
-inductive step, so let's continue unfolding ``exp`` for that case.
-
-.. code-block:: scala
-
- def positive(x: BigInt, y: BigInt): Boolean = {
- require(y >= 0 && x >= 0)
- exp(x, y) >= 0 because {
- if (x == 0) trivial
- else if (y == 0) trivial
- else check { x * exp(x, y - 1) >= 0 }
- }
- }.holds
-
-Although Leon still isn't able to verify the lemma, we now see a way
-to prove the inductive step: ``x`` is positive (by the second
-precondition) and so is ``exp(x, y - 1)`` (by the inductive
-hypothesis). Hence the product ``x * exp(x, y - 1)`` is again
-positive.
-
-.. code-block:: scala
-
- def positive(x: BigInt, y: BigInt): Boolean = {
- require(y >= 0 && x >= 0)
- exp(x, y) >= 0 because {
- if (x == 0) trivial
- else if (y == 0) trivial
- else check {
- x >= 0 && exp(x, y - 1) >= 0 because positive(x, y - 1)
- }
- }
- }.holds
-
-With these hints, Leon is able to verify the proof. Again, we could
-shorten the proof by omitting inequalities that Leon can infer
-directly, albeit at the expense of readability.
-
-.. code-block:: scala
-
- def positiveShort(x: BigInt, y: BigInt): Boolean = {
- require(y >= 0 && x > 0)
- exp(x, y) >= 0 because {
- if (x == 0) trivial
- else if (y == 0) trivial
- else positiveShort(x, y - 1)
- }
- }.holds
-
-We conclude the section with the inductive proof of another, somewhat
-more interesting property of the exponential function, namely that
-:math:`(x y)^z = x^z y^z`.
-
-.. code-block:: scala
-
- def expMultCommute(x: BigInt, y: BigInt, z: BigInt): Boolean = {
- require(z >= 0)
- exp(x * y, z) == exp(x, z) * exp(y, z) because {
- if (x == 0) trivial
- else if (y == 0) trivial
- else if (z == 0) trivial
- else check {
- x * y * exp(x * y, z - 1) ==
- x * exp(x, z - 1) * y * exp(y, z - 1) because
- expMultCommute(x, y, z - 1)
- }
- }
- }.holds
-
-.. _rel-reasoning:
-
-Relational reasoning
-********************
-
-The majority of the example propositions we have seen so far related
-some expression (e.g. ``l.reverse ++ Nil()`` or ``exp(x, y)``) to some
-other expression (e.g. ``... == l1`` or ``... >= 0``). This is
-certainly a common case among the sorts of propositions about
-functions and data structures one might wish to prove. The proofs of
-such propositions typically involve some form of *relational
-reasoning*, i.e. reasoning involving properties (such as transitivity,
-reflexivity or symmetry) of the relations in question. Leon knows
-about these properties for built-in relations such as ``==`` or orders
-on numbers. For user-defined relations, they first need to be
-established as lemmas. In this section, we discuss how to make
-effective use of built-in relations, but the general principles extend
-to their user-defined counterparts.
-
-When working with simple structural equality, we can rely on the default ``==``
-operator and Leon will happily understand when the reflexivity, symmetry and
-transitivity properties apply and use them to conclude bigger proofs. Similarly,
-when working on ``BigInt``, Leon knows about reflexivity, antisymmetry and
-transitivity over ``>=`` or ``<=``, and also antireflexivity, antisymmetry
-and transitivity of ``>`` and ``<``.
-
-However, even for relatively simple proofs about ADTs, Leon needs
-hints when combining, say equality, with user-defined operations, such
-as ``++`` or ``reverse`` on lists. For example, Leon is not able to
-verify that the following holds for arbitrary pairs of lists ``l1``
-and ``l2``:
-
-.. code-block:: scala
-
- (l1 ++ l2).reverse == l2.reverse ++ l1.reverse
-
-The hard part of giving hints to Leon is often to find them in the
-first place. Here we can apply a general principle on top of
-structural induction (as discussed in the previous section): we start
-from the left-hand side of an equation and build a chain of
-intermediate equations to the right-hand side. Using ``check``
-statements we can identify where Leon times out and hence potentially
-needs hints.
-
-.. code-block:: scala
-
- def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
- ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
- l1 match {
- case Nil() =>
- /* 1 */ check { (Nil() ++ l2).reverse == l2.reverse } &&
- /* 2 */ check { l2.reverse == l2.reverse ++ Nil() } &&
- /* 3 */ check { l2.reverse ++ Nil() == l2.reverse ++ Nil().reverse }
- case Cons(x, xs) =>
- /* 4 */ check { ((x :: xs) ++ l2).reverse == (x :: (xs ++ l2)).reverse } &&
- /* 5 */ check { (x :: (xs ++ l2)).reverse == (xs ++ l2).reverse :+ x } &&
- /* 6 */ check { (xs ++ l2).reverse :+ x == (l2.reverse ++ xs.reverse) :+ x } &&
- /* 7 */ check { (l2.reverse ++ xs.reverse) :+ x == l2.reverse ++ (xs.reverse :+ x) } &&
- /* 8 */ check { l2.reverse ++ (xs.reverse :+ x) == l2.reverse ++ (x :: xs).reverse }
- }
- }
- }.holds
-
-If we run the above code with a decent timeout, Leon reports four
-*UNKNOWN* cases: the postcondition of the ``reverseAppend`` function itself and
-checks number 2, 6 and 7.
-
- * Check #2 fails because, as we saw earlier, Leon is not capable of
- guessing the ``rightUnitAppend`` lemma by itself. We fix this case
- by simply instantiating the lemma, i.e. by appending ``&&
- rightUnitAppend(l2.reverse)`` to the base case.
-
- * Check #6 fails because, at this point, we need to inject the
- induction hypothesis on ``xs`` and ``l2`` by adding ``&&
- reverseAppend(xs, l2)``.
-
- * Finally, check #7 fails for a similar reason as check #2: we need
- an additional "associativity" lemma to prove that ``(l1 ++ l2) :+ t
- == l1 ++ (l2 :+ t)`` holds for any ``l1``, ``l2`` and ``t``. We
- call this lemma ``snocAfterAppend`` and leave it as an exercise for
- the reader.
-
-Once we have a valid proof, we can try to optimize it for readability.
-As it stands, the resulting code is rather verbose because both sides
-of most equations are duplicated. One option is to completely remove
-the equations (they are implied by the instantiations of the lemmas)
-and simply write
-
-.. code-block:: scala
-
- def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
- ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
- l1 match {
- case Nil() =>
- rightUnitAppend(l2.reverse)
- case Cons(x, xs) =>
- reverseAppend(xs, l2) && snocAfterAppend(l2.reverse, xs.reverse, x)
- }
- }
- }.holds
-
-Or we can employ the equational reasoning DSL provided by the
-``leon.proofs`` package to remove the duplicate expressions and
-interleave the equations with their associated proofs. This has the
-advantage of not losing information that is still useful for a human
-being reading the proof later on:
-
-.. code-block:: scala
-
- def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
- ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
- l1 match {
- case Nil() => {
- (Nil() ++ l2).reverse ==| trivial |
- l2.reverse ==| rightUnitAppend(l2.reverse) |
- l2.reverse ++ Nil() ==| trivial |
- l2.reverse ++ Nil().reverse
- }.qed
- case Cons(x, xs) => {
- ((x :: xs) ++ l2).reverse ==| trivial |
- (x :: (xs ++ l2)).reverse ==| trivial |
- (xs ++ l2).reverse :+ x ==| reverseAppend(xs, l2) |
- (l2.reverse ++ xs.reverse) :+ x ==|
- snocAfterAppend(l2.reverse, xs.reverse, x) |
- l2.reverse ++ (xs.reverse :+ x) ==| trivial |
- l2.reverse ++ (x :: xs).reverse
- }.qed
- }
- }
- }.holds
-
-The idea is to group statements in a block
-(``{ }``) and call ``qed`` on it. Then, instead of writing ``a == b && b == c
-&& hint1 && hint2`` we write ``a ==| hint1 | b ==| hint2 | c``. And when no
-additional hint is required, we can use ``trivial`` which simply stands for
-``true``.
-
-Additionally, by using this DSL, we get the same feedback granularity from Leon
-as if we had used ``check`` statements. This way we can construct proofs based
-on equality more easily and directly identify where hints are vital.
-
-One shortcoming of the relational reasoning DSL is that it relies on
-Leon's knowledge of the relational properties of the built-in
-relations, and in particular those of equality. Consequently is works
-badly (if at all) with user-defined relations. However, since the DSL
-is defined as a library (in ``library/proof/package.scala``), it can
-in principle be extended and modified to include specific user-defined
-relations on a case-by-case basis.
-
-.. TODO add a word about requirement in ctor (e.g. Rational)
-
-.. TODO Footnote linking to Etienne's answer on SO.
-
-
-Limits of the approach: HOFs, quantifiers and termination
-*********************************************************
-
-While the techniques discussed in this section are useful in general,
-their applicability has of course its limitations in practice. These
-limitations are mostly due to Leon's limited support for certain
-language constructs, such as higher-order functions (HOFs) or
-quantifiers (which in turn is due, mostly, to the limited support of
-the corresponding theories in the underlying SMT solvers).
-
-Still, even using these "experimental" features, one manages to prove
-some interesting propositions. Here is another list example, which
-relates the ``foldLeft``, ``foldRight`` and ``reverse`` operations
-defined on lists and makes crucial use of HOFs:
-
-.. code-block:: scala
-
- import leon.collection._
- import leon.lang._
- import leon.proof._
-
- def folds[A, B](xs: List[A], z: B, f: (B, A) => B): Boolean = {
- val f2 = (x: A, z: B) => f(z, x)
- xs.foldLeft(z)(f) == xs.reverse.foldRight(z)(f2) because {
- xs match {
- case Nil() => true
- case Cons(x, xs) => {
- (x :: xs).foldLeft(z)(f) ==| trivial |
- xs.foldLeft(f(z, x))(f) ==| folds(xs, f(z, x), f) |
- xs.reverse.foldRight(f(z, x))(f2) ==| trivial |
- xs.reverse.foldRight(f2(x, z))(f2) ==|
- snocFoldRight(xs.reverse, x, z, f2) |
- (xs.reverse :+ x).foldRight(z)(f2) ==| trivial |
- (x :: xs).reverse.foldRight(z)(f2)
- }.qed
- }
- }
- }.holds
-
-A rather different, more general issue that arises when proving
-propositions using Leon is related to *termination checking*. When
-verifying inductive proofs (and more generally the postconditions of
-recursive methods), Leon assumes that the corresponding proofs are
-*well-founded*, or equivalently, that the corresponding recursive
-methods terminate on all inputs. Yet Leon does not -- by default --
-check that this is the case. It is thus possible -- and indeed rather
-easy -- to write bogus proofs (intentionally or accidentally) which
-Leon recognizes as valid, but which are not well-founded. Consider
-the following lemma, which apparently establishes that all lists are
-empty:
-
-.. code-block:: scala
-
- import leon.collection._
- import leon.lang._
- import leon.proof._
-
- object NotWellFounded {
-
- // This proof is not well-founded. Since Leon doesn't run the
- // termination checker by default, it will accept the proof as
- // valid.
- def allListsAreEmpty[T](xs: List[T]): Boolean = {
- xs.isEmpty because {
- xs match {
- case Nil() => trivial
- case Cons(x, xs) => allListsAreEmpty(x :: xs)
- }
- }
- }.holds
- }
-
-Leon has (experimental) support for termination checking, which can be
-enabled using the ``--termination`` command line option to minimize
-the risk of accidentally writing bogus proofs such as the one above.
-
-.. TODO example: folds + future work (alt. version of folds)
-
-.. _post-cond:
-
-Techniques for proving non-trivial postconditions
--------------------------------------------------
-
-When proving a mathematical lemma, the return type of the
-corresponding function is most of
-the time, if not always, ``Boolean``. For those proofs it is rather easy to
-write a postcondition: using ``holds`` is generally enough.
-
-But when it comes to writing postconditions for more general functions, such as
-the addition on rational numbers, we are no longer dealing with ``Boolean`` so
-we need a strategy to properly write ``ensuring`` statements.
-
-
-Rationals: a simple example
-***************************
-
-Let's take rational numbers as an example: we define them as a case class with
-two attributes, `n` for the numerator and `d` for the denominator. We also
-define three simple properties on them: ``isRational``, ``isNonZero`` and
-``isPositive``.
-
-.. code-block:: scala
-
- case class Rational(n: BigInt, d: BigInt) {
- def isRational = d != 0
- def isPositive = isRational && (n * d >= 0)
- def isNonZero = isRational && (n != 0)
-
- // ...
- }
-
-And on top of that we want to support addition on ``Rational`` in a way that
-the rationality and positiveness properties are correctly preserved:
-
-.. code-block:: scala
-
- def +(that: Rational): Rational = {
- require(isRational && that.isRational)
- Rational(n * that.d + that.n * d, d * that.d)
- } ensuring { res =>
- res.isRational &&
- (this.isPositive == that.isPositive ==> res.isPositive == this.isPositive)
- }
-
-In this simple case, things work nicely and we can write the
-multiplication in a similar fashion:
-
-.. code-block:: scala
-
- def *(that: Rational): Rational = {
- require(isRational && that.isRational)
- Rational(n * that.n, d * that.d)
- } ensuring { res =>
- res.isRational &&
- (res.isNonZero == (this.isNonZero && that.isNonZero)) &&
- (res.isPositive == (!res.isNonZero || this.isPositive == that.isPositive))
- }
-
-
-Measures: a slightly more complex example
-*****************************************
-
-Now let's look at a slightly more complex example: measures on
-discrete probability spaces. We represent such measures using a
-``List``-like recursive data structure: a generic abstract class
-``Meas[A]`` that has two subclasses, ``Empty[A]`` and ``Cons[A]``.
-The constructor of the class ``Empty[A]`` takes no arguments; it
-represents an "empty" measure that evaluates to 0 when applied to any
-set of values of type ``A``. The constructor of ``Cons[A]``, on the
-other hand, takes three parameters: a value ``x``, its associated
-weight ``w`` expressed as a ``Rational`` (since Leon doesn't quite yet
-support real numbers out of the box), and another measure ``m`` on
-``A``. The value ``Cons(x, w, m)`` represents the measure obtained by
-adding to ``m`` the "single-point" measure that evaluates to ``w`` at
-``x`` and to 0 everywhere else. We also define an ``isMeasure``
-property -- similar to the ``isRational`` property presented above --
-which recursively checks that all the weights in a measure are
-positive rationals (note that all our measures have finite support).
-
-.. code-block:: scala
-
- /** Measures on discrete probability spaces. */
- sealed abstract class Meas[A] {
-
- /** All weights must be positive. */
- def isMeasure: Boolean = this match {
- case Empty() => true
- case Cons(x, w, m) => w.isPositive && m.isMeasure
- }
-
- // ...
- }
-
- /** The empty measure maps every subset of the space A to 0. */
- case class Empty[A]() extends Meas[A]
-
- /**
- * The 'Cons' measure adjoins an additional element 'x' of type 'A'
- * to an existing measure 'm' over 'A'. Note that 'x' might already
- * be present in 'm'.
- */
- case class Cons[A](x: A, w: Rational, m: Meas[A]) extends Meas[A]
-
-
-The defining operation on a measure ``m`` is its evaluation ``m(xs)``
-(or equivalently ``m.apply(xs)``) on some set ``xs: Set[A]``, i.e. on a
-subset of the "space" ``A``. The value of ``m`` should be a positive
-rational for any such set ``xs``, provided ``m.isMeasure`` holds.
-This suggests ``_.isPositive`` as the postcondition for ``apply``,
-but simply claiming that the result is positive is not enough for Leon
-to verify this postcondition.
-
-We can provide the necessary hint to Leon by performing structural
-induction on ``this`` inside the postcondition as follows:
-
-.. code-block:: scala
-
- /** Compute the value of this measure on a subset of the space 'A'. */
- def apply(xs: Set[A]): Rational = {
- require (isMeasure)
- this match {
- case Empty() => Rational(0, 1)
- case Cons(x, w, m) => if (xs contains x) w + m(xs) else m(xs)
- }
- } ensuring { res =>
- res.isPositive because {
- this match {
- case Empty() => trivial
- case Cons(x, w, m) => m(xs).isPositive
- }
- }
- }
-
-Notice the similarity between the pattern match in the body of the
-``apply`` function and that in the postcondition. With this hint,
-Leon is able to verify the postcondition.
-
-
-A complex example: additivity of measures
------------------------------------------
-
-Using the principles and techniques discussed so far, one can prove
-quite advanced propositions using Leon. Returning to the
-measure-theoretic example from the previous section, we would like to
-prove that our implementation of measures is properly *additive*.
-Formally, a measure :math:`\mu \colon A \to \mathbb{R}` on a countable
-set :math:`A` must fulfill the following additivity property
-[#dicrete-meas]_:
-
-.. math::
-
- \forall A_1, A_2 \subseteq A . A_1 \cap A_2 = \emptyset \Rightarrow
- \mu(A_1 \cup A_2) = \mu(A_1) + \mu(A_2)
-
-which we can express in Leon as
-
-.. code-block:: scala
-
- def additivity[A](m: Meas[A], xs: Set[A], ys: Set[A]): Boolean = {
- require(m.isMeasure && (xs & ys).isEmpty)
- m(xs ++ ys) == m(xs) + m(ys)
- }.holds
-
-We can prove this property using structural induction on the parameter
-``m``, case analysis on the parameters ``xs`` and ``ys``, equational
-reasoning, and properties of rational numbers (in the form of
-user-defined lemmas) as well as sets (using Leon's built-in support).
-
-.. code-block:: scala
-
- def additivity[A](m: Meas[A], xs: Set[A], ys: Set[A]): Boolean = {
- require(m.isMeasure && (xs & ys).isEmpty)
- m(xs ++ ys) == m(xs) + m(ys) because {
- m match {
- case Empty() => trivial
- case Cons(x, w, n) => if (xs contains x) {
- w + n(xs ++ ys) ==| additivity(n, xs, ys) |
- w + (n(xs) + n(ys)) ==| plusAssoc(w, n(xs), n(ys)) |
- (w + n(xs)) + n(ys) ==| !(ys contains x) |
- m(xs) + m(ys)
- }.qed else if (ys contains x) {
- w + n(xs ++ ys) ==| additivity(n, xs, ys) |
- w + (n(xs) + n(ys)) ==| plusComm(w, (n(xs) + n(ys))) |
- (n(xs) + n(ys)) + w ==| plusAssoc(n(xs), n(ys), w) |
- n(xs) + (n(ys) + w) ==| plusComm(n(ys), w) |
- n(xs) + (w + n(ys)) ==| !(xs contains x) |
- m(xs) + m(ys)
- }.qed else {
- n(xs ++ ys) ==| additivity(n, xs, ys) |
- n(xs) + n(ys)
- }.qed
- }
- }
- }.holds
-
-The full proof (including the proofs of all helper lemmas) as well as
-its generalization to *sub-additivity* can be found in the
-``testcases/verification/proof/measure/`` directory of the Leon
-distribution [#example-dir]_.
-
-
-Quick Recap
------------
-
-Let's summarize what we've learned here. To write proofs efficiently,
-it's good to keep the following in mind:
-
-1. Always use a proper timeout and ask Leon for more information about
- what he tries to verify, e.g. ``--timeout=5 --debug=verification``.
-
-2. Use ``@induct`` when working on structurally inductive proofs to
- get a more precise feedback from Leon: this will decompose the
- proof into a base case and an inductive case for the first argument
- of the function under consideration.
-
- If Leon isn't able to verify the proof using ``@induct``, try
- performing manual case analysis.
-
-3. Modularize your proofs and verify *sub-goals*!
-
- - use plenty of helper lemmas;
- - use ``check`` abundantly;
- - if possible use the relational reasoning DSL presented above.
-
- This is especially handy when you can connect the two sides of a relational
- claim with sub-statements.
-
-
-.. rubric:: Footnotes
-
-.. [#example-dir] The source code of this example and all other in
- this chapter are included in the Leon distribution. Examples about
- lists can be found in ``library/collection/List.scala``, the other
- examples are located in the ``testcases/verification/proof/``
- directory.
-
-.. [#props-not-types] Perhaps surprisingly, propositions and proofs
- live in the same universe in Leon. This is contrary to
- e.g. type-theoretic proof assistants where propositions are
- represented by types and proofs are terms inhabiting such types.
-
-.. [#dicrete-meas] To be precise, we are assuming here the underlying
- measurable space :math:`(A, \mathcal{P}(A))`, where :math:`A` is
- countable and :math:`\mathcal{P}(A)` denotes its discrete σ-algebra
- (i.e. the power set of :math:`A`).
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
deleted file mode 100644
index 38f18d0aef81eea7dd1006c92fda59f170b3f25e..0000000000000000000000000000000000000000
--- a/src/sphinx/options.rst
+++ /dev/null
@@ -1,375 +0,0 @@
-.. _cmdlineoptions:
-
-Command Line Options
-====================
-
-Leon's command line options have the form ``--option`` or ``--option=value``.
-To enable a flag option, use ``--option=true`` or ``on`` or ``yes``,
-or just ``--option``. To disable a flag option, use ``--option=false``
-or ``off`` or ``no``.
-
-Additionally, if you need to pass options to the ``scalac`` frontend of Leon,
-you can do it by using a single dash ``-``. For example, try ``-Ybrowse:typer``.
-
-The rest of this section presents command-line options that Leon recognizes.
-For a short (but always up-to-date) summary, you can also invoke ``leon --help``.
-
-Choosing which Leon feature to use
-----------------------------------
-
-The first group of options determine which feature of Leon will be used.
-These options are mutually exclusive (except when noted). By default, ``--verify`` is chosen.
-
-* ``--eval``
-
- Evaluates parameterless functions and value definitions.
-
-* ``--verify``
-
- Proves or disproves function contracts, as explained in the :ref:`verification` section.
-
-* ``--repair``
-
- Runs program :ref:`repair <repair>`.
-
-* ``--synthesis``
-
- Partially synthesizes ``choose()`` constructs (see :ref:`synthesis` section).
-
-* ``--termination``
-
- Runs termination analysis. Can be used along ``--verify``.
-
-* ``--inferInv``
-
- Infer invariants from the (instrumented) code (using Orb).
-
-* ``--instrument``
-
- Instrument the code for inferring time/depth/stack bounds (using Orb).
-
-* ``--genc``
-
- Translate a Scala program into C99 equivalent code (see :ref:`genc` section); requires
- ``--xlang``.
-
-* ``--noop``
-
- Runs the program through the extraction and preprocessing phases, then outputs it in the specified
- directory. Used mostly for debugging purposes.
-
-* ``--help``
-
- Prints a helpful message, then exits.
-
-
-
-Additional top-level options
-----------------------------
-
-These options are available to all Leon components:
-
-* ``--debug=d1,d2,...``
-
- Enables printing detailed messages for the components d1,d2,... .
- Available components are:
-
- * ``datagen`` (Data generators)
-
- * ``eval`` (Evaluators)
-
- * ``genc`` (C code generation)
-
- * ``isabelle`` (:ref:`The Isabelle-based solver <isabelle>`)
-
- * ``leon`` (The top-level component)
-
- * ``options`` (Options parsed by Leon)
-
- * ``positions`` (When printing, attach positions to trees)
-
- * ``repair`` (Program repair)
-
- * ``solver`` (SMT solvers and their wrappers)
-
- * ``synthesis`` (Program synthesis)
-
- * ``termination`` (Termination analysis)
-
- * ``timers`` (Timers, timer pools)
-
- * ``trees`` (Manipulation of trees)
-
- * ``types`` (When printing, attach types to expressions)
-
- * ``verification`` (Verification)
-
- * ``xlang`` (Transformation of XLang into Pure Scala programs)
-
-
-* ``--functions=f1,f2,...``
-
- Only consider functions f1, f2, ... . This applies to all functionalities
- where Leon manipulates the input in a per-function basis.
-
- Leon will match against suffixes of qualified names. For instance:
- ``--functions=List.size`` will match the method ``leon.collection.List.size``,
- while ``--functions=size`` will match all methods and functions named ``size``.
- This option supports ``_`` as wildcard: ``--functions=List._`` will
- match all ``List`` methods.
-
-* ``--solvers=s1,s2,...``
-
- Use solvers s1, s2,... . If more than one solver is chosen, all chosen
- solvers will be used in parallel, and the best result will be presented.
- By default, the ``fairz3`` solver is picked.
-
- Some solvers are specialized in proving verification conditions
- and will have hard time finding a counterexample in case of an invalid
- verification condition, whereas some are specialized in finding
- counterexamples, and some provide a compromise between the two.
- Also, some solvers do not as of now support higher-order functions.
-
- Available solvers include:
-
- * ``enum``
-
- Uses enumeration-based techniques to discover counterexamples.
- This solver does not actually invoke an SMT solver,
- and operates entirely on the level of Leon trees.
-
- * ``fairz3``
-
- Native Z3 with z3-templates for unfolding recursive functions (default).
-
- * ``smt-cvc4``
-
- CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding
- of recursive functions, handling of lambdas etc. To use this or any
- of the following CVC4-based solvers, you need to have the ``cvc4``
- executable in your system path (the latest unstable version is recommended).
-
- * ``smt-cvc4-cex``
-
- CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only.
- Recursive functions are not unrolled, but encoded through the
- ``define-funs-rec`` construct available in the new SMTLIB-2.5 standard.
- Currently, this solver does not handle higher-order functions.
-
- * ``smt-cvc4-proof``
-
- CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
- ``smt-cvc4-cex``.
- Currently, this solver does not handle higher-order functions.
-
- * ``smt-z3``
-
- Z3 through SMT-LIB. To use this or the next solver, you need to
- have the ``z3`` executable in your program path (the latest stable version
- is recommended). Inductive reasoning happens on the Leon side
- (similarly to ``smt-cvc4``).
-
- * ``smt-z3-q``
-
- Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
- instead encoded with universal quantification.
- For example, ``def foo(x:A) = e`` would be encoded by asserting
-
- .. math::
-
- \forall (x:A). foo(x) = e
-
- even if ``e`` contains an invocation to ``foo``.
-
- Currently, this solver does not handle higher-order functions.
-
- * ``unrollz3``
-
- Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
-
- * ``ground``
-
- Only solves ground verification conditions (without variables) by evaluating them.
-
- * ``isabelle``
-
- Solve verification conditions via Isabelle.
-
-* ``--strict``
-
- Terminate Leon after each phase if a non-fatal error is encountered
- (such as a failed verification condition). By default, this option is activated.
-
-* ``--timeout=t``
-
- Set a timeout for each attempt to prove one verification condition/
- repair one function (in sec.)
-
-* ``--xlang``
-
- Support for additional language constructs described in :ref:`xlang`.
- These constructs are desugared into :ref:`purescala` before other operations,
- except for the ``--genc`` option which uses the original constructs to generate
- :ref:`genc`.
-
-Additional Options (by component)
----------------------------------
-
-The following options relate to specific components in Leon. Bear in mind
-that related components might still use these options, e.g. repair,
-which invokes synthesis and verification, will also use
-synthesis options and verification options.
-
-Verification
-************
-
-* ``--parallel``
-
- Check verification conditions in parallel.
-
-File Output
-***********
-
-* ``--o=dir``
-
- Output files to the directory ``dir`` (default: leon.out).
- Used when ``--noop`` is selected.
-
- When used with ``--genc`` this option designates the output *file*.
-
-Code Extraction
-***************
-
-* ``--strictCompilation``
-
- Do not try to recover after an error in compilation and exit Leon.
-
-Synthesis
-*********
-
-* ``--cegis:opttimeout``
-
- Consider a time-out of CE-search as untrusted solution.
-
-* ``--cegis:shrink``
-
- Shrink non-deterministic programs when tests pruning works well.
-
-* ``--cegis:vanuatoo``
-
- Generate inputs using new korat-style generator.
-
-* ``--costmodel=cm``
-
- Use a specific cost model for this search.
- Available: ``Naive``, ``WeightedBranches``
-
-* ``--derivtrees``
-
- Generate a derivation tree for every synthesized function.
- The trees will be output in ``*.dot`` files.
-
-* ``--manual=cmd``
-
- Override Leon's automated search through the space of programs during synthesis.
- Instead, the user can navigate the program space manually
- by choosing which deductive synthesis rules is instantiated each time.
-
- The optional ``cmd`` argument is a series of natural numbers in the form
- ``n1,n1,...,nk``. It represents the series of command indexes that the search
- should instantiate at the beginning of the search.
- Useful for repeated search attempts.
-
-Fair-z3 Solver
-**************
-
-* ``--checkmodels``
-
- Double-check counter-examples with evaluator.
-
-* ``--codegen``
-
- Use compiled evaluator instead of interpreter.
-
-* ``--evalground``
-
- Use evaluator on functions applied to ground arguments.
-
-* ``--feelinglucky``
-
- Use evaluator to find counter-examples early.
-
-* ``--unrollcores``
-
- Use unsat-cores to drive unrolling while remaining fair.
-
-CVC4 Solver
-***********
-
-* ``--solver:cvc4=<cvc4-opt>``
-
- Pass extra command-line arguments to CVC4.
-
-Isabelle
-********
-
-* ``--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.
-
-Invariant Inference
-*******************
-
-These options are to be used in conjunction with ``--inferInv`` and ``--instrument``.
-
-* ``--cegis``
-
- Use cegis instead of farkas
-
-* ``--disableInfer``
-
- Disable automatic inference of auxiliary invariants
-
-* ``--fullunroll``
-
- Unroll all calls in every unroll step
-
-* ``--inferTemp``
-
- Infer templates by enumeration
-
-* ``--minbounds``
-
- Tighten the inferred time bounds
-
-* ``--stats-suffix=s``
-
- Specifies the suffix of the statistics file
-
-* ``--usereals``
-
- Interpret the input program as a program over real numbers
-
-* ``--wholeprogram``
-
- Perform a non-modular whole program analysis
-
-* ``--withmult``
-
- Do not convert multiplication into a recursive function inside verification conditions
-
diff --git a/src/sphinx/purescala.rst b/src/sphinx/purescala.rst
deleted file mode 100644
index 7cde91421d3a77cfc68162b6c643e4396a8bc85b..0000000000000000000000000000000000000000
--- a/src/sphinx/purescala.rst
+++ /dev/null
@@ -1,519 +0,0 @@
-.. _purescala:
-
-Pure Scala
-==========
-
-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
-performs additional checks to ensure that the given program
-belongs to Pure Scala.
-
-Pure Scala supports two kinds of top-level declarations:
-
-1. Algebraic Data Type (ADT) definitions in the form of an
- abstract class and case classes/objects
-
-.. code-block:: scala
-
- abstract class MyList
- case object MyEmpty extends MyList
- case class MyCons(elem: BigInt, rest: MyList) extends MyList
-
-2. Objects/modules, for grouping classes and functions
-
-.. code-block:: scala
-
- object Specs {
- def increment(a: BigInt): BigInt = {
- a + 1
- }
-
- case class Identifier(id: BigInt)
- }
-
-.. _adts:
-
-
-Boolean
-#######
-
-Booleans are used to express truth conditions in Leon.
-Unlike some proof assistants, there is no separation
-at the type level between
-Boolean values and the truth conditions of conjectures
-and theorems.
-
-Typical propositional operations are available using Scala
-notation, along
-with a new shorthand for implication. The `if` expression
-is also present.
-
-.. code-block:: scala
-
- a && b
- a || b
- a == b
- !a
- a ==> b // Leon syntax for boolean implication
-
-Leon uses short-circuit interpretation of `&&`, `||`, and `==>`,
-which evaluates the second argument only when needed:
-
-.. code-block:: scala
-
- a && b === if (a) b else false
-
- a || b === if (a) true else b
-
- a ==> b === if (a) b else true
-
-This aspect is important because of:
-
-1. evaluation of expressions, which is kept compatible with Scala
-
-2. verification condition generation for safety: arguments of Boolean operations
-may be operations with preconditions; these preconditions apply only in case
-that the corresponding argument is evaluated.
-
-3. termination checking, which takes into account that only one of the paths in an if expression is evaluated for a given truth value of the condition.
-
-
-Algebraic Data Types
---------------------
-
-Abstract Classes
-****************
-
-ADT roots need to be defined as abstract, unless the ADT is defined with only one case class/object. Unlike in Scala, abstract classes cannot define fields or constructor arguments.
-
-.. code-block:: scala
-
- abstract class MyType
-
-An abstract class can be extended by other abstract classes.
-
-Case Classes
-************
-
-The abstract root can also be extended by a case-class, defining several fields:
-
-.. code-block:: scala
-
- case class MyCase1(f: Type, f2: MyType) extends MyType
- case class MyCase2(f: Int) extends MyType
-
-.. note::
- You can also define single case-class, for Tuple-like structures.
-
-Case Objects
-************
-
-It is also possible to defined case objects, without fields:
-
-.. code-block:: scala
-
- case object BaseCase extends MyType
-
-
-Generics
---------
-
-Leon supports type parameters for classes and functions.
-
-.. code-block:: scala
-
- object Test {
- abstract class List[T]
- case class Cons[T](hd: T, tl: List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
- def contains[T](l: List[T], el: T) = { ... }
- }
-
-
-.. note::
- Type parameters are always **invariant**. It is not possible to define ADTs like:
-
- .. code-block:: scala
-
- abstract class List[T]
- case class Cons[T](hd: T, tl: List[T]) extends List[T]
- case object Nil extends List[Nothing]
-
- Leon in fact restricts type parameters to "simple hierarchies", where subclasses define the same type parameters in the same order.
-
-Methods
--------
-
-You can define methods in classes.
-
-.. code-block:: scala
-
- abstract class List[T] {
- def contains(e: T) = { .. }
- }
- case class Cons[T](hd: T, tl: List[T]) extends List[T]
- case object Nil extends List[Nothing]
-
- def test(a: List[Int]) = a.contains(42)
-
-It is possible to define abstract methods in abstract classes and implement them in case classes.
-It is also possible to override methods.
-
-.. code-block:: scala
-
- abstract class A {
- def x(a: Int): Int
- }
-
- abstract class B extends A {
- def x(a: Int) = {
- require(a > 0)
- 42
- } ensuring { _ >= 0 }
- }
-
- case class C(c: Int) extends B {
- override def x(i: Int) = {
- require(i >= 0)
- if (i == 0) 0
- else c + x(i-1)
- } ensuring ( _ == c * i )
- }
-
- case class D() extends B
-
-It is not possible, however, to call methods of a superclass with the ``super`` keyword.
-
-Specifications
---------------
-
-Leon supports three kinds of specifications to functions and methods:
-
-Preconditions
-*************
-
-Preconditions constraint the argument and is expressed using `require`. It should hold for all calls to the function.
-
-.. code-block:: scala
-
- def foo(a: Int, b: Int) = {
- require(a > b)
- ...
- }
-
-Postconditions
-**************
-
-Postconditions constraint the resulting value, and is expressed using `ensuring`:
-
-.. code-block:: scala
-
- def foo(a: Int): Int = {
- a + 1
- } ensuring { res => res > a }
-
-Body Assertsions
-****************
-
-Assertions constrain intermediate expressions within the body of a function.
-
-.. code-block:: scala
-
- def foo(a: Int): Int = {
- val b = -a
- assert(a >= 0 || b >= 0, "This will fail for -2^31")
- a + 1
- }
-
-The error description (last argument of ``assert``) is optional.
-
-Expressions
------------
-
-Leon supports most purely-functional Scala expressions:
-
-Pattern matching
-****************
-
-.. code-block:: scala
-
- expr match {
- // Simple (nested) patterns:
- case CaseClass( .. , .. , ..) => ...
- case v @ CaseClass( .. , .. , ..) => ...
- case v : CaseClass => ...
- case (t1, t2) => ...
- case 42 => ...
- case _ => ...
-
- // can also be guarded, e.g.
- case CaseClass(a, b, c) if a > b => ...
- }
-
-Custom pattern matching with ``unapply`` methods are also supported:
-
-.. code-block:: scala
-
- object :: {
- def unapply[A](l: List[A]): Option[(A, List[A])] = l match {
- case Nil() => None()
- case Cons(x, xs) => Some((x, xs))
- }
- }
-
- def empty[A](l: List[A]) = l match {
- case x :: xs => false
- case Nil() => true
- }
-
-Values
-******
-
-.. code-block:: scala
-
- val x = ...
-
- val (x, y) = ...
-
- val Cons(h, _) = ...
-
-.. note::
- The latter two cases are actually syntactic sugar for pattern matching with one case.
-
-
-Inner Functions
-***************
-
-.. code-block:: scala
-
- def foo(x: Int) = {
- val y = x + 1
- def bar(z: Int) = {
- z + y
- }
- bar(42)
- }
-
-
-Predefined Types
-****************
-
-TupleX
-######
-
-.. code-block:: scala
-
- val x = (1,2,3)
- val y = 1 -> 2 // alternative Scala syntax for Tuple2
- x._1 // == 1
-
-
-Int
-###
-
-.. code-block:: scala
-
- a + b
- a - b
- -a
- a * b
- a / b
- a % b // a modulo b
- a < b
- a <= b
- a > b
- a >= b
- a == b
-
-.. note::
- Integers are treated as 32bits integers and are subject to overflows.
-
-BigInt
-######
-
-.. code-block:: scala
-
- val a = BigInt(2)
- val b = BigInt(3)
-
- -a
- a + b
- a - b
- a * b
- a / b
- a % b // a modulo b
- a < b
- a > b
- a <= b
- a >= b
- a == b
-
-.. note::
- BigInt are mathematical integers (arbitrary size, no overflows).
-
-Real
-####
-
-``Real`` represents the mathematical real numbers (different from floating points). It is an
-extension to Scala which is meant to write programs closer to their true semantics.
-
-.. code-block:: scala
-
- val a: Real = Real(2)
- val b: Real = Real(3, 5) // 3/5
-
- -a
- a + b
- a - b
- a * b
- a / b
- a < b
- a > b
- a <= b
- a >= b
- a == b
-
-.. note::
- Real have infinite precision, which means their properties differ from ``Double``.
- For example, the following holds:
-
- .. code-block:: scala
-
- def associativity(x: Real, y: Real, z: Real): Boolean = {
- (x + y) + z == x + (y + z)
- } holds
-
- While it does not hold with floating point arithmetic.
-
-
-Set
-###
-
-.. code-block:: scala
-
- import leon.lang.Set // Required to have support for Sets
-
- val s1 = Set(1,2,3,1)
- val s2 = Set[Int]()
-
- s1 ++ s2 // Set union
- s1 & s2 // Set intersection
- s1 -- s2 // Set difference
- s1 subsetOf s2
- s1 contains 42
-
-
-Functional Array
-################
-
-.. code-block:: scala
-
- val a = Array(1,2,3)
-
- a(index)
- a.updated(index, value)
- a.length
-
-
-Map
-###
-
-.. code-block:: scala
-
- import leon.lang.Map // Required to have support for Maps
-
- val m = Map[Int, Boolean](42 -> false)
-
- m(index)
- m isDefinedAt index
- m contains index
- m.updated(index, value)
- m + (index -> value)
- m + (value, index)
- m.get(index)
- m.getOrElse(index, value2)
-
-
-Function
-########
-
-.. code-block:: scala
-
- val f1 = (x: Int) => x + 1 // simple anonymous function
-
- val y = 2
- val f2 = (x: Int) => f1(x) + y // closes over `f1` and `y`
- val f3 = (x: Int) => if (x < 0) f1 else f2 // anonymous function returning another function
-
- list.map(f1) // functions can be passed around ...
- list.map(f3(1) _) // ... and partially applied
-
-.. note::
- No operators are defined on function-typed expressions, so specification is
- currently quite limited.
-
-
-Symbolic Input-Output examples
-------------------------------
-
-Sometimes, a complete formal specification is hard to write,
-especially when it comes to simple, elementary functions. In such cases,
-it may be easier to provide a set of IO-examples. On the other hand,
-IO-examples can never cover all the possible executions of a function,
-and are thus weaker than a formal specification.
-
-Leon provides a powerful compromise between these two extremes.
-It introduces *symbolic IO-examples*, expressed through a specialized ``passes``
-construct, which resembles pattern-matching:
-
-.. code-block:: scala
-
- sealed abstract class List {
-
- def size: Int = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
- }) ensuring { res => (this, res) passes {
- case Nil() => 0
- case Cons(_, Nil()) => 1
- case Cons(_, Cons(_, Nil())) => 2
- }}
- }
- case class Cons[T](h: T, t: List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
-
-In the above example, the programmer has chosen to partially specify ``size``
-through a list of IO-examples, describing what the function should do
-for lists of size 0, 1 or 2.
-Notice that the examples are symbolic, in that the elements of the lists are
-left unconstrained.
-
-The semantics of ``passes`` is the following.
-Let ``a: A`` be a tuple of method parameters and/or ``this``, ``b: B``,
-and for each i ``pi: A`` and ``ei: B``. Then
-
-.. code-block:: scala
-
- (a, b) passes {
- case p1 => e1
- case p2 => e2
- ...
- case pN => eN
- }
-
-is equivalent to
-
-.. code-block:: scala
-
- a match {
- case p1 => b == e1
- case p2 => b == e2
- ...
- case pN => b == eN
- case _ => true
- }
diff --git a/src/sphinx/r b/src/sphinx/r
deleted file mode 100755
index d210288c6c7b8e7cbb94f8591be3af6d2c4c32e6..0000000000000000000000000000000000000000
--- a/src/sphinx/r
+++ /dev/null
@@ -1 +0,0 @@
-make html
diff --git a/src/sphinx/references.rst b/src/sphinx/references.rst
deleted file mode 100644
index cc161cfdcb163dc7731a4f9c7b54771ef902cc3f..0000000000000000000000000000000000000000
--- a/src/sphinx/references.rst
+++ /dev/null
@@ -1,41 +0,0 @@
-.. _references:
-
-References
-==========
-
-The Leon system is documented in several papers and talks, which provide additional information on the algorithms and techniques we used in Leon.
-
-
-Videos
-******
-
- - `Verifying and Synthesizing Software with Recursive Functions <http://video.itu.dk/video/10044793/icalp-2014-viktor-kuncak>`_ (ICALP 2014)
- - `Executing Specifications using Synthesis and Constraint Solving <http://videos.rennes.inria.fr/ConferenceRV2013/indexViktorKuncak.html>`_ (RV 2013)
- - `Video of Verifying Programs in Leon <http://youtu.be/JFbx4iryNb0>`_ (2013)
-
-
-Papers
-******
-
- - `Translating Scala Programs to Isabelle/HOL (System Description) <http://lara.epfl.ch/~kuncak/papers/HupelKuncak16TranslatingScalaProgramsIsabelleHOLSystemDescription.pdf>`_, by *Lars Hupel* and *Viktor Kuncak*. International Joint Conference on Automated Reasoning (IJCAR), 2016.
- - `Counter-example complete verification for higher-order functions <http://lara.epfl.ch/~kuncak/papers/VoirolETAL15CounterExampleCompleteVerificationHigherOrderFunctions.pdf>`_, by *Nicolas Voirol*, *Etienne Kneuss*, and *Viktor Kuncak*. Scala Symposium, 2015.
- - `Sound reasoning about integral data types with a reusable SMT solver interface <http://lara.epfl.ch/~kuncak/papers/BlancKuncak15SoundReasoningIntegralDataTypes.pdf>`_, by *Régis Blanc* and *Viktor Kuncak*. Scala Symposium, 2015.
- - `Deductive program repair <http://lara.epfl.ch/~kuncak/papers/KneussETAL15DeductiveProgramRepair.pdf>`_, by *Etienne Kneuss*, *Manos Koukoutos*, and *Viktor Kuncak*. Computer-Aided Verification (CAV), 2015.
- - `Symbolic resource bound inference for functional programs <http://lara.epfl.ch/~kuncak/papers/MadhavanKuncak14SymbolicResourceBoundInferenceFunctionalPrograms.pdf>`_, by *Ravichandhran Madhavan* and *Viktor Kuncak*. Computer Aided Verification (CAV), 2014.
- - `Checking data structure properties orders of magnitude faster <http://lara.epfl.ch/~kuncak/papers/KoukoutosKuncak14CheckingDataStructurePropertiesOrdersMagnitudeFaster.pdf>`_, by *Emmanouil Koukoutos* and *Viktor Kuncak*. Runtime Verification (RV), 2014
- - `Synthesis Modulo Recursive Functions <http://lara.epfl.ch/~kuncak/papers/KneussETAL13SynthesisModuloRecursiveFunctions.pdf>`_, by *Etienne Kneuss*, *Viktor Kuncak*, *Ivan Kuraj*, and *Philippe Suter*. OOPSLA 2013
- - `Executing specifications using synthesis and constraint solving (invited talk) <http://lara.epfl.ch/~kuncak/papers/KuncakETAL13ExecutingSpecificationsSynthesisConstraintSolvingInvitedTalk.pdf>`_, by Viktor Kuncak, Etienne Kneuss, and Philippe Suter. Runtime Verification (RV), 2013
- - `An Overview of the Leon Verification System <http://lara.epfl.ch/~kuncak/papers/BlancETAL13VerificationTranslationRecursiveFunctions.pdf>`_, by *Régis Blanc*, *Etienne Kneuss*, *Viktor Kuncak*, and *Philippe Suter*. Scala Workshop 2013
- - `Reductions for synthesis procedures <http://lara.epfl.ch/~kuncak/papers/JacobsETAL13ReductionsSynthesisProcedures.pdf>`_, by *Swen Jacobs*, *Viktor Kuncak*, and *Phillippe Suter*. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013
- - `Constraints as Control <http://lara.epfl.ch/~kuncak/papers/KoeksalETAL12ConstraintsControl.pdf>`_, *Ali Sinan Köksal*, *Viktor Kuncak*, *Philippe Suter*, Principles of Programming Languages (POPL), 2012
- - `Satisfiability Modulo Recursive Programs <http://lara.epfl.ch/~kuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf>`_, by *Philippe Suter*, *Ali Sinan Köksal*, *Viktor Kuncak*, Static Analysis Symposium (SAS), 2011
- - `Scala to the power of Z3: Integrating SMT and programming <http://lara.epfl.ch/~kuncak/papers/KoeksalETAL11ScalaZ3.pdf>`_, by *Ali Sinan Köksal*, *Viktor Kuncak*, and *Philippe Suter*. Computer-Aideded Deduction (CADE) Tool Demo, 2011
- - `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*.
diff --git a/src/sphinx/repair.rst b/src/sphinx/repair.rst
deleted file mode 100644
index 614f829d002dab76381a28c7d382262ad2daace5..0000000000000000000000000000000000000000
--- a/src/sphinx/repair.rst
+++ /dev/null
@@ -1,176 +0,0 @@
-.. _repair:
-
-Repair
-======
-
-Leon can repair buggy :ref:`Pure Scala <purescala>` programs.
-Given a specification and an erroneous implementation for a function,
-Leon will localize the cause of the bug and provide an alternative solution.
-In the following we will give some insight into how repair works
-through a simple example.
-
-An example
------------
-
-In the following code, a user has tried to implement a function
-that performs natural number division using only addition and subtraction.
-However, this snippet contains a bug:
-
-.. code-block:: scala
-
- def moddiv(a: Int, b: Int): (Int, Int) = {
- require(a >= 0 && b > 0);
- if (b > a) {
- (1, 0) // fixme: should be (a, 0)
- } else {
- val (r1, r2) = moddiv(a-b, b)
- (r1, r2+1)
- }
- } ensuring {
- res => b*res._2 + res._1 == a
- }
-
-Leon can discover and repair this error.
-Invoking ``leon --repair --functions=moddiv`` will yield: ::
-
- [ Info ] ======================= 1. Discovering tests for moddiv =======================
- [ Info ] - Passing: 1
- [ Info ] - Failing: 5
- [ Info ] - Minimal Failing Set Size: 2
- [ Info ] Finished in 836ms
- [ Info ] ==================== 2. Locating/Focusing synthesis problem ====================
- [ Info ] Program size : 152
- [ Info ] Original body size: 30
- [ Info ] Focused expr size : 3
- [ Info ] Finished in 78ms
- [ Info ] =============================== 3. Synthesizing ===============================
- [ Info ] ⟦ a;b, ↓ moddiv(a, b) && ⊙ {(1, 0)} && a >= 0 && b > 0 && b > a ≺ ⟨ val res = x27;
- [ Info ] b * res._2 + res._1 == a ⟩ x27 ⟧
- [ Info ] [CEGLESS ] ⟦ a;b, ↓ moddiv(a, b) && ⊙ {(1, 0)} && a >= 0 && b > 0 && b > a ≺
- [ Info ] ⟨ val res = x27; b * res._2 + res._1 == a ⟩ x27 ⟧
- [ Info ] [CEGLESS ] Solved with: ⟨ true | (a, 0) ⟩...
- [ Info ] Finished in 1995ms
- [ Info ] Found trusted solution!
- [ Info ] ============================== Repair successful: ==============================
- [ Info ] --------------------------------- Solution 1: ---------------------------------
- [ Info ] (a, 0)
- [ Info ] ================================= In context: =================================
- [ Info ] --------------------------------- Solution 1: ---------------------------------
- [ Info ] def moddiv(a : Int, b : Int): (Int, Int) = {
- require(a >= 0 && b > 0)
- if (b > a) {
- (a, 0)
- } else {
- val (r1, r2) = moddiv(a - b, b)
- (r1, (r2 + 1))
- }
- } ensuring {
- (res : (Int, Int)) => (b * res._2 + res._1 == a)
- }
-
-Leon has localized the error on the expression ``(1, 0)`` and provided
-the correct alternative ``(a, 0)``, as well as the entire repaired function
-(due to some implementation restrictions,
-the function body which Leon outputs is a little more complex than
-the one given above, but equivalent to it).
-
-Repair Mechanism
-----------------
-
-We can break down the repair mechanism of Leon in three phases:
-
-Test Case Generation
-********************
-
-In the beginning, Leon will try to generate test cases which will
-help localize the error. Sample inputs are generated by an enumeration
-technique, and then the function under repair is executed on them.
-The test cases are divided in passing (those that satisfy the function
-specification) and failing. What we are actually interested in are
-the failing test cases; if none are generated, we resort to an SMT
-solver to discover a counterexample for the function (or possibly
-prove it correct).
-
-Next, a dependency analysis is run on the discovered failing tests,
-and those that recursively invoke the function with another failing input
-are rejected.
-
-Fault Localization
-******************
-
-In the next step, Leon will try to localize the problem to the smallest
-possible subexpression of the function body. The idea is to run the failing
-test cases through the function and isolate the paths followed by some erroneous
-executions. In ``moddiv``, Leon will successfully identify the expression ``(1, 0)``
-as the source of the error. Repair will work even in the presence of more than one
-errors; however, the discovered subexpression may be larger. This is compensated
-for in a later stage.
-
-Because of this approach, repair works better for programs
-that contain a small number of localized errors.
-Errors that wrap the whole body of the function will fail to be localized,
-and repair will fall back to generic synthesis.
-
-Synthesis of the Repaired Expression
-************************************
-
-Leon then tries to synthesize an alternative expression in place of the
-erroneous one which satisfies the function specification. To this, it uses
-generic :ref:`synthesis`, enhanced with a rule for similar term exploration,
-due to our hypothesis of small localized errors.
-
-Verification of the synthesized solution
-****************************************
-
-Finally, Leon will try to verify the synthesized solution. In case of
-failure to prove it correct (but also to disprove it), Leon will still
-present it as an untrusted solution.
-
-Repairing with IO-examples
---------------------------
-
-In the :ref:`Pure Scala <purescala>` section, we have presented the ``passes`` construct.
-This construct is especially useful when it comes to repair. Look at the following example:
-
-.. code-block:: scala
-
- sealed abstract class List {
- def drop(i: Int): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
- case (Cons(h, t), ) =>
- t // FIXME should be this
- case (Cons(_, t), i) =>
- t.drop(i) //FIXME should be i-1
- }} ensuring { res => ((this, i), res) passes {
- case (Cons(_, Nil()), 42) => Nil()
- case (l@Cons(_, _), 0) => l
- case (Cons(a, Cons(b, Nil())), 1) => Cons(b, Nil())
- case (Cons(a, Cons(b, Cons(c, Nil()))), 2) => Cons(c, Nil())
- }}
- }
- case class Cons[T](h: T, t: List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
-
-In the above example, the programmer has chosen to specify drop through a
-list of IO-examples, describing what the function should do in the cases where
-the elements to drop are more than the size of the list,
-or 0, 1 or 2 elements are to be dropped by a list with enough elements.
-
-Leon manages to repair this program: ::
-
- ...
- [ Info ] Found trusted solution!
- [ Info ] ============================== Repair successful: ==============================
- [ Info ] --------------------------------- Solution 1: ---------------------------------
- [ Info ] val scrut = ($this, i);
- [ Info ] scrut match {
- [ Info ] case (Nil(), _) =>
- [ Info ] Nil[T]()
- [ Info ] case (Cons(h, t), 0) =>
- [ Info ] scrut._1
- [ Info ] case (Cons(_, t), i) =>
- [ Info ] t.drop(i - 1)
- [ Info ] }
- ...
-
diff --git a/src/sphinx/synthesis.rst b/src/sphinx/synthesis.rst
deleted file mode 100644
index 17ed8eab14623f8fb09cc2ac04e73b55e4700209..0000000000000000000000000000000000000000
--- a/src/sphinx/synthesis.rst
+++ /dev/null
@@ -1,448 +0,0 @@
-.. _synthesis:
-
-Synthesis
-=========
-
-Software synthesis offers an alternative way of developing trustworthy
-programs. At a high level, program specifications describe **what** the
-function should do, and its corresponding implementation describes **how** it
-will do it. While verification ensures that both views match, synthesis
-consists of translating these specifications (or expectations) to executable
-programs which realises them.
-
-As we have seen previously, relatively precise specifications of complex
-operations can be written concisely. Synthesis can thus reduce development time
-and allows the user to focus on high-level aspects.
-
-Deductive Synthesis Framework
------------------------------
-
-The synthesizer takes a synthesis problem that it extracts from ``choose`` or
-holes (``???``) found in the program. Formally, we define a **synthesis problem** as
-
-.. math::
-
- [[ ~~ \bar{a} ~~ \langle ~~ \Pi \rhd \phi ~~ \rangle ~~ \bar{x} ~~ ]]
-
-
-which carries the following information:
-
- * a set of input variables :math:`\bar{a}`, initially all variables in scope of the ``choose``,
- * a set of output variables :math:`\bar{x}`, corresponding to the values to synthesize,
- * a path-condition :math:`\Pi`, constraining :math:`\bar{a}`,
- * the specification :math:`\phi` relating input variables to output variables.
-
-The job of the synthesizer is to convert this problem into a solution :math:`[ ~ P ~ | ~ T ~ ]`, which consists of
-
- * a executable program term :math:`T` (an expression that may contain input variables),
- * a precondition :math:`P` under which this program is valid
-
-To illustrate, we consider the following program:
-
-.. code-block:: scala
-
- def foo(a: BigInt, b: BigInt): Int = {
- if (a > b) {
- choose ( (x: BigInt) => x > a)
- } else {
- 0
- }
- }
-
-
-From this program, we will extract the following initial synthesis problem:
-
-.. math::
-
- [[ ~~ a, b ~~ \langle ~~ a > b ~ \rhd ~ x > a ~~ \rangle ~~ x ~~ ]]
-
-A possible solution to this problem would be:
-
-.. math::
-
- [ ~ \top ~ | ~ a + 1 ~ ]
-
-To solve this problem, the synthesizer will apply a series of rules which will
-try to either
-
- 1. Decompose this problem into sub problems, which may be simpler to solve
- 2. Immediately find a solution
-
-
-This corresponds to an and-or graph of rule applications, which Leon will
-explore.
-
-
-Decomposing Rules
------------------
-
-Leon defines several rules that decompose a synthesis problem (a ``choose``)
-into sub-problems that may be simpler to solve. Such rules also define a way to
-generate a solution for the original problem, when provided with solutions for
-all of the sub-problems. These rules thus both decompose the problems and
-recompose the solutions. Leon defines several of such decomposing rules:
-
-Equality Split
-^^^^^^^^^^^^^^
-
-Given two input variables `a` and `b` of compatible types, this rule
-considers the cases where `a = b` and `a != b`. From:
-
-.. code-block:: scala
-
- choose(res => spec(a, b, res))
-
-
-this rule generates two sub-chooses, and combines them as follows:
-
-.. code-block:: scala
-
- if (a == b) {
- choose(res => spec(a, a, res))
- } else {
- choose(res => spec(a, b, res))
- }
-
-
-Inequality Split
-^^^^^^^^^^^^^^^^
-
-Given two input variables `a` and `b` of numeric type, this rule
-considers the cases where `a < b`, `a == b`, and `a > b`. From:
-
-.. code-block:: scala
-
- choose(res => spec(a, b, res))
-
-
-this rule generates three sub-chooses, and combines them as follows:
-
-.. code-block:: scala
-
- if (a < b) {
- choose(res => spec(a, b, res))
- } else if (a > b) {
- choose(res => spec(a, b, res))
- } else {
- choose(res => spec(a, a, res))
- }
-
-
-ADT Split
-^^^^^^^^^
-
-Given a variable `a` typed as an algebraic data type `T`, the rules decomposes
-the problem in cases where each case correspond to one subtype of `T`:
-
-.. code-block:: scala
-
- abstract class T
- case class A(f1: Int) extends T
- case class B(f2: Boolean) extends T
- case object C extends T
-
- choose(res => spec(a, res))
-
-
-this rule generates three sub-chooses, in which the input variable `a` is
-substituted by the appropriate case, and combines them as follows:
-
-.. code-block:: scala
-
- a match {
- case A(f1) => choose(res => spec(A(f1), res))
- case B(f2) => choose(res => spec(B(f2), res))
- case C => choose(res => spec(C, res))
- }
-
-
-Int Induction
-^^^^^^^^^^^^^
-
-Given an Int (or BigInt) variable `a`, the rules performs induction on `a`:
-
-.. code-block:: scala
-
- choose(res => spec(a, res))
-
-
-this rule generates three sub-chooses, one for the base case and one for each inductive case (we allow negative numbers):
-
-.. code-block:: scala
-
- def tmp1(a: Int) = {
- if (a == 0) {
- choose(res => spec(a, res))
- } else if (a > 0) {
- val r1 = tmp1(a-1)
- choose(res => spec(a, res))
- } else if (a < 0) {
- val r1 = tmp1(a+1)
- choose(res => spec(a, res))
- }
- }
-
- tmp1(a)
-
-This allows Leon to synthesize a well-structured recursive function.
-
-One Point
-^^^^^^^^^
-
-This syntactic rule considers equalities of an output variable at the top level of the
-specification, and substitutes the variable with the corresponding expression in
-the rest of the formula. Given the following specification:
-
-.. math::
- res1 = expr \land \phi
-
-and assuming :math:`expr` does not use :math:`a`, we generate the alternative and
-arguable simpler specification:
-
-
-.. math::
- \phi[res1 \rightarrow expr]
-
-
-Assert
-^^^^^^
-
-The `Assert` rule scans the specification for predicates that only constraint
-input variables and lifts them out of the specification. Since these are
-constraints over the input variables, they typically represent the
-precondition necessary for the ``choose`` to be feasible.
-Given an input variable `a`:
-
-.. code-block:: scala
-
- choose(res => spec(a, res) && pred(a))
-
-will become:
-
-.. code-block:: scala
-
- require(pred(a))
-
- choose(res => spec(a, res))
-
-Case Split
-^^^^^^^^^^
-
-This rule considers a top-level disjunction and decomposes it:
-
-.. code-block:: scala
-
- choose(res => spec1(a, res) || spec2(a, res))
-
-thus becomes two sub-chooses
-
-.. code-block:: scala
-
- if (P) {
- choose(res => spec1(a, res))
- } else {
- choose(res => spec2(a, res))
- }
-
-Here we note that ``P`` is not known until the first ``choose`` is solved, as it
-corresponds to its precondition.
-
-
-
-Equivalent Input
-^^^^^^^^^^^^^^^^
-
-This rule discovers equivalences in the input variables in order to eliminate
-redundancies. We consider two kinds of equivalences:
-
- 1) Simple equivalences: the specification contains :math:`a = b` at the top
- level.
-
- 2) ADT equivalence the specification contains :math:`l.isInstanceOf[Cons]
- \land h = l.head \land t = l.tail` which entails :math:`l = Cons(h, t)` and
- thus allows us to substitute :math:`l` by :math:`Cons(h, t)`.
-
-Eliminating equivalences prevents explosion of redundant rule instantiations.
-For instance, if you have four integer variables where three of them are
-equivalent, Leon has 6 ways of applying `Inequality Split`. After
-eliminating equivalences, only one application remains possible.
-
-Unused Input
-^^^^^^^^^^^^
-
-This rule tracks input variables (variables originally in scope of the
-``choose``) that are not constrained by the specification or the
-path-condition. These input variables carry no information and are thus
-basically useless. The rule consequently eliminates them from the set of input
-variables with which rules may be instantiated.
-
-Unconstrained Output
-^^^^^^^^^^^^^^^^^^^^
-
-This rule is the dual of ``Unused Input``: it tracks output variable (result
-values) that are not constrained. Such variables can be trivially synthesized
-by any value or expression of the right type. For instance:
-
-.. code-block:: scala
-
- choose ((x: Int, y: T) => spec(y))
-
-becomes
-
-.. code-block:: scala
-
- (0, choose ((y: T) => spec(y)))
-
-Leon will use the simplest value of the given type, when available. Note this
-rule is not able to synthesize variables of generic types, as no literal values
-exist for these. While ``null`` may be appropriate in Scala, Leon does not
-define it.
-
-..
- Unification.DecompTrivialClash,
- Disunification.Decomp,
- ADTDual,
- CaseSplit,
- IfSplit,
- DetupleOutput,
- DetupleInput,
- InnerCaseSplit
-
-Closing Rules
--------------
-
-While decomposing rules split problems in sub-problems, Leon also defines rules
-that are able to directly solve certain synthesis problems. These rules are
-crucial for the synthesis search to terminate efficiently. We define several
-closing rules that apply in different scenarios:
-
-Ground
-^^^^^^
-
-This rule applies when the synthesis problem has no input variables. If the
-specification is satisfiable, its model corresponds to a valid solution. We
-rely on SMT solvers to check satisfiability of the formulas. For instance:
-
-.. code-block:: scala
-
- choose ((x: Int, y: Int) => x > 42 && y > x)
-
-can trivially be synthesized by ``(1000, 1001)``.
-
-If the specification turns out to be UNSAT, the synthesis problem is impossible
-and we synthesize it as an ``error`` with a ``false`` precondition.
-
-
-Optimistic Ground
-^^^^^^^^^^^^^^^^^
-
-This rule acts like `Ground`, but without the requirement on the absence of input
-variables. The reasoning is that even though the problem has input variables,
-the solutions might still be a constant expression.
-
-`Optimistic Ground` also tries to satisfy the specification, but it also needs
-to validate the resulting model. That is, given a valuation of output
-variables, it checks whether it exists a valuation for input variables such that
-the specification is violated. The model is discarded if such counter-example
-is found. If no counter-example exist, we solve the synthesis problem with the
-corresponding values.
-
-The rule tries at most three times to discover a valid value.
-
-CEGIS
-^^^^^
-
-`CEGIS` stands for Counter-Example-Guided Inductive Synthesis, it explores the
-space of small expressions to find valid solutions. Here we represent the space
-of programs by a tree, where branches are determined by free boolean variables.
-For instance, a tree for small integer operations could be:
-
-.. code-block:: scala
-
- def res(b, a1, a2) = if (b1) 0
- else if (b2) 1
- else if (b3) a1
- else if (b4) a2
- else if (b5) c1(b, a1, a2) + c2(b, a1, a2)
- else c1(b, a1, a2) * c2(b, a1, a2)
-
- def c1(b, a1, a2) = if (b7) 0
- else if (b8) 1
- else if (b9) a1
- else a2
-
- def c2(b, a1, a2) = if (b10) 0
- else if (b11) 1
- else if (b12) a1
- else a2
-
-At a high-level, it consists of the following loop:
-
- 1. Find one expression and inputs that satisfies the specification:
- :math:`\exists \bar{b}, a1, a2. spec(a1, a2, res(\bar{b}, a1, a2))`.
- If this fails, we know that the solution is not in the search space.
- If this succeeds, we:
-
- 2. Validate the expression represented by :math:`M_\bar{b}` for all inputs by
- searching for a counter-example: :math:`\exists a1, a2. \lnot spec(a1, a2, res(M_\bar{b}, a1, a2))`.
- If such counter-example exists, start over with (1) with this program
- excluded. If no counter-example exists we found a valid expression.
-
-The space of expressions our CEGIS rule considers is small expressions of
-bounded depth (3), which contain for each type: a few literals, functions and
-operations returning that type that do not transitively call the function under
-synthesis (to prevent infinite loops), and recursive calls where one argument is
-decreasing.
-
-
-TEGIS
-^^^^^
-
-This rule uses the same search space as `CEGIS` but relies only on tests
-(specified by the user or generated) to validate expressions. It is thus a
-generally faster way of discovering candidate expressions. However, these
-expressions are not guaranteed to be valid since they have only been validated
-by tests. Leon's synthesis framework supports untrusted solutions which trigger
-an end-to-end validation step that relies on verification.
-
-
-String Conversion
-^^^^^^^^^^^^^^^^^
-
-This rule applies to pretty-printing problems given a non-empty list of examples, i.e. of the type:
-
-.. code-block:: scala
-
- choose ((x: String) =>
- (input, x) passes {
- case InputExample1 => "Output Example1"
- case InputExample2 => "Output Example2"
- }
- )
-
-It will create a set of functions and an expression that will be consistent with the example. The example need to ensure the following properties:
-
-* **Primitive display**: All primitive values (int, boolean, Bigint) present in the InputExample must appear in the OutputExample. The exception being Boolean which can also be rendered differently (e.g. as "yes" and "no")
-* **Linearization**: The output example must use the same order as the definition of InputExample; that is, no Set, Map or out of order rendering (e.g. ``case (1, 2) => "2, 1"`` will not work)
-
-To further optimize the search, it is also better to ensure the following property
-
-* **Constant case class display**: By default, if a hierarchy of case classes only contains parameterless variants, such as
-
-.. code-block:: scala
-
- abstract class StackThread
- case class T1() extends StackThread
- case class T2() extends StackThread
-
-it will first try to render expressions with the following function:
-
-.. code-block:: scala
-
- def StackThreadToString(t: StackThread) = t match {
- case T1() => "T1"
- case T2() => "T2"
- }
- CONST + StackThreadToString(t) + CONST
-
-where CONST will be inferred from the examples.
diff --git a/src/sphinx/themes/leon/layout.html b/src/sphinx/themes/leon/layout.html
deleted file mode 100644
index fd901cd19be7bc150fe540b9078642467b1a1e9f..0000000000000000000000000000000000000000
--- a/src/sphinx/themes/leon/layout.html
+++ /dev/null
@@ -1,90 +0,0 @@
-{#
- leon/layout.html
- ~~~~~~~~~~~~~~~~~
-#}
-{%- extends "agogo/layout.html" %}
-
-{% block header %}
- <div class="header-wrapper">
- <div class="header">
- <div class="left">
- {%- block headertitle %}
- <div class="headertitle"><a
- href="{{ pathto(master_doc) }}">{{ shorttitle|e }}</a></div>
- {%- endblock %}
- <div class="rel">
- {%- if prev %}
- <a href="{{ prev.link|e }}">{{ prev.title }}</a> |
- {%- endif %}
- <a class="uplink" href="{{ pathto(master_doc) }}">{{ _('Contents') }}</a>
- {%- if next %}
- | <a href="{{ next.link|e }}">{{ next.title }}</a>
- {%- endif %}
- </div>
- </div>
- {%- block sidebarsearch %}
- <div class="right">
- <form class="search" action="{{ pathto('search') }}" method="get">
- <input type="text" name="q" placeholder="Search.." />
- <input type="submit" value="{{ _('Go') }}" />
- <input type="hidden" name="check_keywords" value="yes" />
- <input type="hidden" name="area" value="default" />
- </form>
- </div>
- {%- endblock %}
- <div class="clearer"></div>
- </div>
- </div>
-{% endblock %}
-
-{% block content %}
- <div class="content-wrapper">
- <div class="content">
- <div class="document">
- {%- block document %}
- {{ super() }}
- {%- endblock %}
- </div>
- <div class="sidebar">
- {%- block sidebartoc %}
- <h3>{{ _('Table Of Contents') }}</h3>
- {{ toctree() }}
- {%- endblock %}
- </div>
- <div class="clearer"></div>
- </div>
- </div>
-{% endblock %}
-
-{% block footer %}
- <div class="footer-wrapper">
- <div class="footer">
- <div class="left">
- {%- if show_source and has_source and sourcename %}
- <a href="{{ pathto('_sources/' + sourcename, true)|e }}"
- rel="nofollow">{{ _('Show Source') }}</a>
- {%- endif %}
- </div>
-
- <div class="right">
- {%- if show_copyright %}
- {%- if hasdoc('copyright') %}
- {% trans path=pathto('copyright'), copyright=copyright|e %}© <a href="{{ path }}">Copyright</a> {{ copyright }}.{% endtrans %}
- {%- else %}
- {% trans copyright=copyright|e %}© Copyright {{ copyright }}.{% endtrans %}
- {%- endif %}
- {%- endif %}
- {%- if last_updated %}
- {% trans last_updated=last_updated|e %}Last updated on {{ last_updated }}.{% endtrans %}
- {%- endif %}
- {%- if show_sphinx %}
- {% trans sphinx_version=sphinx_version|e %}Created using <a href="http://sphinx-doc.org/">Sphinx</a> {{ sphinx_version }}.{% endtrans %}
- {%- endif %}
- </div>
- <div class="clearer"></div>
- </div>
- </div>
-{% endblock %}
-
-{% block relbar1 %}{% endblock %}
-{% block relbar2 %}{% endblock %}
diff --git a/src/sphinx/themes/leon/static/css/leon.css_t b/src/sphinx/themes/leon/static/css/leon.css_t
deleted file mode 100644
index 0d2d025ab08c55316ba19342ab55ee117f8d51cb..0000000000000000000000000000000000000000
--- a/src/sphinx/themes/leon/static/css/leon.css_t
+++ /dev/null
@@ -1,536 +0,0 @@
-* {
- margin: 0px;
- padding: 0px;
-}
-
-body {
- font-family: {{ theme_bodyfont }};
- line-height: 1.4em;
- color: black;
- background-color: {{ theme_bgcolor }};
-}
-
-pre {
- line-height: 1.3em;
-}
-
-
-/* Page layout */
-
-div.header, div.content, div.footer {
- width: {{ theme_pagewidth }};
- margin-left: auto;
- margin-right: auto;
-}
-
-div.header-wrapper {
- background: {{ theme_headerbg }};
- border-bottom: 3px solid #2e3436;
-}
-
-
-/* Default body styles */
-a {
- color: {{ theme_linkcolor }};
-}
-
-div.bodywrapper a, div.footer a {
- text-decoration: underline;
-}
-
-.clearer {
- clear: both;
-}
-
-.left {
- float: left;
-}
-
-.right {
- float: right;
-}
-
-.line-block {
- display: block;
- margin-top: 1em;
- margin-bottom: 1em;
-}
-
-.line-block .line-block {
- margin-top: 0;
- margin-bottom: 0;
- margin-left: 1.5em;
-}
-
-h1, h2, h3, h4 {
- font-family: {{ theme_headerfont }};
- font-weight: normal;
- color: {{ theme_headercolor2 }};
- margin-bottom: .8em;
-}
-
-h1 {
- color: {{ theme_headercolor1 }};
-}
-
-h2 {
- padding-bottom: .5em;
- border-bottom: 1px solid {{ theme_headercolor2 }};
-}
-
-a.headerlink {
- visibility: hidden;
- color: #dddddd;
- padding-left: .3em;
-}
-
-h1:hover > a.headerlink,
-h2:hover > a.headerlink,
-h3:hover > a.headerlink,
-h4:hover > a.headerlink,
-h5:hover > a.headerlink,
-h6:hover > a.headerlink,
-dt:hover > a.headerlink {
- visibility: visible;
-}
-
-img {
- border: 0;
-}
-
-div.admonition {
- margin-top: 10px;
- margin-bottom: 10px;
- border: 1px solid #CCC;
-}
-
-div.admonition p {
- padding: 4px;
-}
-
-div.admonition div.highlight {
- margin: 4px;
-}
-
-p.admonition-title {
- background: #CCC;
- font-weight: bold;
- color: white;
-}
-
-dt:target, .highlighted {
- background-color: #fbe54e;
-}
-
-/* Header */
-
-div.header {
- padding-top: 10px;
- padding-bottom: 10px;
-}
-
-div.header .headertitle {
- font-family: {{ theme_headerfont }};
- font-weight: normal;
- font-size: 180%;
- letter-spacing: .08em;
- margin-bottom: .2em;
-}
-
-div.header .headertitle a {
- color: white;
-}
-
-div.header div.rel {
- font-size: 0.8em;
-}
-
-div.header div.rel a {
- color: {{ theme_headerlinkcolor }};
- letter-spacing: .1em;
- text-transform: uppercase;
-}
-
-p.logo {
- float: right;
-}
-
-img.logo {
- border: 0;
-}
-
-
-/* Content */
-div.content-wrapper {
- background-color: white;
- padding-top: 20px;
- padding-bottom: 20px;
-}
-
-div.document {
- width: 55em;
- float: right;
-}
-
-div.body {
- padding-right: 2em;
- text-align: {{ theme_textalign }};
-}
-
-div.document h1 {
- line-height: 120%;
-}
-
-div.document ul {
- margin: 1.5em;
- list-style-type: square;
-}
-
-div.document dd {
- margin-left: 1.2em;
- margin-top: .4em;
- margin-bottom: 1em;
-}
-
-div.document .section {
- margin-top: 1.7em;
-}
-div.document .section:first-child {
- margin-top: 0px;
-}
-
-div.document div.highlight {
- padding: 3px;
- background-color: #eeeeec;
- border-top: 2px solid #dddddd;
- border-bottom: 2px solid #dddddd;
- margin-top: .8em;
- margin-bottom: .8em;
-}
-
-div.document h2 {
- margin-top: .7em;
-}
-
-div.document p {
- margin-bottom: .5em;
-}
-
-div.document li.toctree-l1 {
-}
-
-div.document .toctree-wrapper ul {
- margin: 0.5em 1.5em;
-}
-
-div.document .descname {
- font-weight: bold;
-}
-
-div.document .docutils.literal {
- background-color: #eeeeec;
- padding: 1px;
-}
-
-div.document .docutils.xref.literal {
- background-color: transparent;
- padding: 0px;
-}
-
-div.document blockquote {
- margin: 1em;
-}
-
-div.document ol {
- margin: 1.5em;
-}
-
-
-/* Sidebar */
-
-div.sidebar {
- width: 15em;
- float: left;
- font-size: .9em;
-}
-
-div.sidebar a, div.header a {
- text-decoration: none;
-}
-
-div.sidebar a:hover, div.header a:hover {
- text-decoration: underline;
-}
-
-div.sidebar h3 {
- color: #2e3436;
- text-transform: uppercase;
- font-size: 130%;
- letter-spacing: .1em;
-}
-
-div.sidebar ul {
- list-style-type: none;
-}
-
-div.sidebar li.toctree-l1 a {
- display: block;
- padding: 1px;
- border: 1px solid #dddddd;
- background-color: #eeeeec;
- margin-bottom: .4em;
- padding-left: 3px;
- color: #2e3436;
-}
-
-div.sidebar li.toctree-l2 a {
- background-color: transparent;
- border: none;
- margin-left: 1em;
- border-bottom: 1px solid #dddddd;
-}
-
-div.sidebar li.toctree-l3 a {
- background-color: transparent;
- border: none;
- margin-left: 2em;
- border-bottom: 1px solid #dddddd;
-}
-
-div.sidebar li.toctree-l2:last-child a {
- border-bottom: none;
-}
-
-div.sidebar li.toctree-l1.current > a {
- background: {{ theme_headerbg }};
- color: white;
-}
-
-div.sidebar li.toctree-l1.current li.toctree-l2 a {
- border-right: none;
-}
-
-div.sidebar input[type="text"] {
- width: 170px;
-}
-
-div.sidebar input[type="submit"] {
- width: 30px;
-}
-
-
-/* Footer */
-
-div.footer-wrapper {
- background: {{ theme_footerbg }};
- border-top: 4px solid #babdb6;
- padding-top: 10px;
- padding-bottom: 10px;
-}
-
-div.footer, div.footer a {
- color: #ccc;
-}
-
-div.footer .right {
- float: right;
- text-align: right;
-}
-
-div.footer .left {
- display: none;
- text-transform: uppercase;
-}
-
-
-/* Styles copied from basic theme */
-
-img.align-left, .figure.align-left, object.align-left {
- clear: left;
- float: left;
- margin-right: 1em;
-}
-
-img.align-right, .figure.align-right, object.align-right {
- clear: right;
- float: right;
- margin-left: 1em;
-}
-
-img.align-center, .figure.align-center, object.align-center {
- display: block;
- margin-left: auto;
- margin-right: auto;
-}
-
-.align-left {
- text-align: left;
-}
-
-.align-center {
- text-align: center;
-}
-
-.align-right {
- text-align: right;
-}
-
-div.header form.search {
- margin-right: 20px;
-}
-
-div.header form.search input {
- padding: 3px;
- color: #555;
- background-color: #fff;
- background-image: none;
- border: 1px solid #ccc;
- border-radius: 4px;
- box-shadow: inset 0 1px 1px rgba(0,0,0,.075);
- transition: border-color ease-in-out .15s,box-shadow ease-in-out .15s;
-}
-
-div.header form.search input[type="text"] {
-}
-
-/* -- search page ----------------------------------------------------------- */
-
-ul.search {
- margin: 10px 0 0 20px;
- padding: 0;
-}
-
-ul.search li {
- padding: 5px 0 5px 20px;
- background-image: url(file.png);
- background-repeat: no-repeat;
- background-position: 0 7px;
-}
-
-ul.search li a {
- font-weight: bold;
-}
-
-ul.search li div.context {
- color: #888;
- margin: 2px 0 0 30px;
- text-align: left;
-}
-
-ul.keywordmatches li.goodmatch a {
- font-weight: bold;
-}
-
-/* -- index page ------------------------------------------------------------ */
-
-table.contentstable {
- width: 90%;
-}
-
-table.contentstable p.biglink {
- line-height: 150%;
-}
-
-a.biglink {
- font-size: 1.3em;
-}
-
-span.linkdescr {
- font-style: italic;
- padding-top: 5px;
- font-size: 90%;
-}
-
-/* -- general index --------------------------------------------------------- */
-
-table.indextable td {
- text-align: left;
- vertical-align: top;
-}
-
-table.indextable dl, table.indextable dd {
- margin-top: 0;
- margin-bottom: 0;
-}
-
-table.indextable tr.pcap {
- height: 10px;
-}
-
-table.indextable tr.cap {
- margin-top: 10px;
- background-color: #f2f2f2;
-}
-
-img.toggler {
- margin-right: 3px;
- margin-top: 3px;
- cursor: pointer;
-}
-
-/* -- viewcode extension ---------------------------------------------------- */
-
-.viewcode-link {
- float: right;
-}
-
-.viewcode-back {
- float: right;
- font-family:: {{ theme_bodyfont }};
-}
-
-div.viewcode-block:target {
- margin: -1px -3px;
- padding: 0 3px;
- background-color: #f4debf;
- border-top: 1px solid #ac9;
- border-bottom: 1px solid #ac9;
-}
-
-@media only screen
-and (max-device-width : 768px) {
- body {
- background: white !important;
- }
- div.sidebar {
- display:none;
- }
- div.document {
- padding-left: 10px;
- padding-right: 10px;
- width: 100% !important;
- float: none !important;
- }
-}
-
-table {
- width: 100%;
- max-width: 100%;
- margin-bottom: 20px;
- background-color: transparent;
- border-spacing: 0;
- border-collapse: collapse;
- border: 0px;
-}
-
-table>tbody>tr>td, table>tbody>tr>th, table>tfoot>tr>td, table>tfoot>tr>th, table>thead>tr>td, table>thead>tr>th {
- padding: 8px;
- line-height: 1.42857143;
- vertical-align: top;
- border-top: 1px solid #ddd;
- border-left: 0px;
- border-right: 0px;
- border-bottom: 0px;
-}
-
-table>thead>tr:first-child>th {
- border-top: 0;
- border-bottom: 2px solid #ddd;
-}
-
-table>tbody>tr:nth-of-type(odd) {
- background-color: #f9f9f9;
-}
-table>tbody>tr:hover {
- background-color: #f5f5f5;
-}
diff --git a/src/sphinx/themes/leon/theme.conf b/src/sphinx/themes/leon/theme.conf
deleted file mode 100644
index a66475c1dbbf3cf511bb61f702b912e3a80d9fb3..0000000000000000000000000000000000000000
--- a/src/sphinx/themes/leon/theme.conf
+++ /dev/null
@@ -1,4 +0,0 @@
-[theme]
-inherit = agogo
-stylesheet = css/leon.css
-pygments_style = trac
diff --git a/src/sphinx/tutorial.rst b/src/sphinx/tutorial.rst
deleted file mode 100644
index d0f26fe4e78c7a074f0214bbad75af93a8c51e5b..0000000000000000000000000000000000000000
--- a/src/sphinx/tutorial.rst
+++ /dev/null
@@ -1,736 +0,0 @@
-.. _tutorial:
-
-Tutorial: Sorting
-=================
-
-This tutorial shows how to:
-
- * use `ensuring`, `require`, and `holds` constructs
- * learn the difference between `Int` and `BigInt`
- * use the `choose` construct for synthesis and constraint solving
- * define lists as algebraic data types
- * use sets and recursive function to specify data structures
- * synthesize insertion into a sorted list
- * synthesize sorting on lists
- * repair an incorrect function
-
-We 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`.
-
-Warm-up: Max
-------------
-
-As a warm-up illustrating verification, we define and debug a `max` function
-and specify its properties. Leon uses Scala constructs
-`require` and `ensuring` to document preconditions and
-postconditions of functions. Note that, in addition to
-checking these conditions at run-time (which standard Scala
-does), Leon can analyze the specifications statically and
-prove them for *all* executions, or, if they are wrong, automatically find
-inputs for which the conditions fail. (Moreover, it can
-execute specifications alone without the code,
-it can do synthesis, and repair.)
-
-Consider the following definition inside an object `TestMax`.
-
-.. code-block:: scala
-
- object TestMax {
- def max(x: Int, y: Int): Int = {
- val d = x - y
- if (d > 0) x
- else y
- } ensuring(res =>
- x <= res && y <= res && (res == x || res == y))
- }
-
-A Leon program consists of one or more modules delimited by
-`object` and `class` declarations.
-The code of `max` attempts to compute maximum of two given arguments
-by subtracting them. If the result is positive, it returns
-the first one, otherwise, it returns the second one.
-
-To specify the correctness of the computed result, we use
-the `ensuring` clause. In this case, the clause specifies
-that the result is larger than `x` and than `y`, and that it
-equals to one of them. The construct `ensuring(res => P)`
-denotes that, if we denote by `res` the return value of the
-function, then `res` satisfies the boolean-valued expression
-`P`. The name `res` we chose is an arbitrary bound variable
-(even though we often tend to use `res`).
-
-We can evaluate this code on some values by writing
-parameterless functions and inspecting what they evaluate
-to. The web interface will display these results for us.
-
-.. code-block:: scala
-
- def test1 = max(10, 5)
- def test2 = max(-5, 5)
- def test3 = max(-5, -7)
-
-The code seems to work correctly on the example values.
-However, Leon automatically finds that it is not correct,
-showing us a counter-example inputs, such as
-
-.. code-block:: scala
-
- x -> -1639624704
- y -> 1879048192
-
-We may wish to define a test method
-
-.. code-block:: scala
-
- def test4 = max(-1639624704, 1879048192)
-
-whose evaluation indeed results in `ensuring` condition being violated.
-The problem is due to overflow of 32-bit integers, due to which
-the value `d` becomes positive, even though `x` is negative and thus smaller than
-the large positive value `y`.
-As in Scala, the `Int` type denotes 32-bit
-integers with the usual signed arithmetic operations from
-computer architecture and the JVM specification.
-
-To use unbounded integers, we simply change the types to
-`BigInt`, obtaining a program that verifies (and, as
-expected, passes all the test cases).
-
-.. code-block:: scala
-
- def max(x: BigInt, y: BigInt): BigInt = {
- val d = x - y
- if (d > 0) x
- else y
- } ensuring(res =>
- x <= res && y <= res && (res == x || res == y))
-
-As a possibly simpler specification, we could have also
-defined the reference implementation
-
-.. code-block:: scala
-
- def rmax(x: BigInt, y: BigInt) = {
- if (x <= y) y else x
- }
-
-and then used as postcondition of `max` simply
-
-.. code-block:: scala
-
- ensuring (res => res == rmax(x,y))
-
-In general, Leon uses both function body and function
-specification when reasoning about the function and its
-uses. Thus, we need not repeat in the postcondition those
-aspects of function body that follow directly through
-inlining the function, but we may wish to state those
-that require induction to prove.
-
-The fact that we can use functions in preconditions
-and postconditions allows us to state fairly general
-properties. For example, the following lemma verifies
-a number of algebraic properties of `max`.
-
-.. code-block:: scala
-
- def max_lemma(x: BigInt, y: BigInt, z: BigInt): Boolean = {
- max(x,x) == x &&
- max(x,y) == max(y,x) &&
- max(x,max(y,z)) == max(max(x,y), z) &&
- max(x,y) + z == max(x + z, y + z)
- } holds
-
-Here `holds` operator on the function body is an
-abbreviation for the postcondition stating that the returned
-result is always true, that is, for
-
-.. code-block:: scala
-
- ensuring(res => res==true)
-
-As a guideline, we typically use `holds` to express such
-algebraic properties that relate multiple invocations of
-functions, whereas we use `ensuring` to document property of
-an arbitrary single invocation of a function. Leon is more likely to automatically
-use the property of a function if it is associated with it using
-`ensuring` than using an external lemma.
-
-Going back to our buggy implementation of `max` on `Int`-s,
-an alternative to using `BigInt`-s is to decide that
-the method should only be used under certain conditions,
-such as `x` and `y` being non-negative. To specify the
-conditions on input, we use the `require` clause.
-
-.. code-block:: scala
-
- def max(x: Int, y: Int): Int = {
- require(0 <= x && 0 <= y)
- val d = x - y
- if (d > 0) x
- else y
- } ensuring (res =>
- x <= res && y <= res && (res == x || res == y))
-
-This program verifies and indeed works correctly on
-non-negative 32-bit integers as inputs.
-
-**Question:** What if we restrict the inputs to `max` to be
-`a)` non-positive, or `b)` strictly negative? Modify the
-`require` clause for each case accordingly and explain the
-behavior of Leon.
-
-In the sequel we will mostly use `BigInt` types.
-
-Let us now look at synthesis. Suppose we omit
-the implementation of `max`, keeping the specification
-in the ensuring clause but using only a placeholder
-`???[BigInt]` indicating we are looking for an unknown implementation
-of an integer type.
-
-.. code-block:: scala
-
- def max(x: BigInt, y: BigInt): BigInt = {
- ???[BigInt]
- } ensuring(res => (res == x || res == y) && x <= res && y <= res)
-
-Leon can then automatically generate an implementation that satisfies
-this specification, such as
-
-.. code-block:: scala
-
- if (y <= x) {
- x
- } else {
- y
- }
-
-This is remarkable because we have much more freedom in
-writing specifications: we can explain the intention of the
-computation using a conjunction of orthogonal properties,
-and still obtain automatically an efficient implementation.
-
-As a remark, an expression with missing parts in Leon is
-an abbreviation for Leon's `choose` construct. Using `choose`
-we can write the above example as
-
-.. code-block:: scala
-
- def max(x: BigInt, y: BigInt): BigInt = choose((res:BigInt) =>
- (res == x || res == y) && x <= res && y <= res)
-
-We explain `choose` in more detail through our subsequent examples.
-
-Sorting Two Elements
---------------------
-
-As a step towards sorting, let us specify a function that
-sorts **two** mathematical integers. Here is what we need to
-write.
-
-.. code-block:: scala
-
- import leon.lang.Set
- import leon.lang.synthesis._
- object Sort {
- def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
- Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
- }
- }
-
-We use `import` to
-include core constructs that are specific to Leon. Note
-that, with the definitions in `leon._` packages, Leon
-programs should also compile with the standard Scala
-compiler. In that sense, Leon is a proper subset of Scala.
-
-Our initial function that "sorts" two mathematical integers
-is named `sort2`. Namely, it accepts two arguments, `x` and
-`y`, and returns a tuple, which we will here denote `res`,
-which stores either `(x,y)` or `(y,x)` such that the first
-component is less than equal the second component.
-
-Note that we use `BigInt` to denote unbounded mathematical
-integers.
-
-As usual in Scala, we write `res._1` for the first component
-of the return tuple `res`, and `res._2` for the second
-component of the tuple.
-
-The specification says that the set of arguments is equal to
-the set consisting of the returned tuple elements. The
-notation `Set(x1,x2,...,xN)` denotes
-
-.. math::
-
- \{ x_1, \ldots, x_N \}
-
-that is, a finite set containing precisely the elements
-`x1`, `x2`,..., `xN`.
-
-Finally, the `choose` construct takes a variable name (here,
-`res`) denoting the value of interest and then gives, after
-the `=>` symbol, a property that this value should
-satisfy. We can read `choose{(x:T) => P}` as
-
-**choose x of type T such that P**
-
-Here, we are interested in computing a result `res` tuple
-such that the set of elements in the tuple is the same as
-`{x,y}` and that the elements are in ascending order in the
-tuple. The specification thus describes sorting of lists of
-length two. Note that the result is uniquely specified, no
-matter what the values of `x` and `y` are.
-
-Evaluating exppressions containing choose
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-Leon's built-in evaluator also works for `choose`
-constructs. To see it in action in the web interface, just
-define a function without parameters, such as
-
-.. code-block:: scala
-
- def testSort2 = sort2(30, 4)
-
-Hovering over `testSort2` should display the computed result
-`(4,30)`. (From :ref:`cmdlineoptions`, use `--eval`.)
-
-Thanks to the ability to execute `choose` constructs Leon
-supports programming with fairly general
-constraints. Executing the `choose` construct is, however,
-expensive. Moreover, the execution times are not very
-predictable. This is why it is desirable to eventually
-replace your `choose` constructs with more efficient
-code. Leon can automate this process in some cases, using
-**synthesis**.
-
-Synthesizing Sort for Two Elements
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-Instead of executing `choose` using a constraint solver
-during execution, we can alternatively instruct Leon to
-synthesize a function corresponding to `choose`. The system
-then synthesizes a computation that satisfies the
-specification, such as, for, example:
-
-.. code-block:: scala
-
- def sort2(x : BigInt, y : BigInt): (BigInt, BigInt) = {
- if (x < y)
- (x, y)
- else
- (y, x)
- }
-
-Depending on the particular run, Leon may also produce a solution such as
-
-.. code-block:: scala
-
- def sort2(x : BigInt, y : BigInt): (BigInt, BigInt) = {
- if (x < y) {
- (x, y)
- } else if (x == y) {
- (x, x)
- } else {
- (y, x)
- }
- }
-
-This code performs some unnecessary case analysis, but still
-satisfies our specification. In this case, the specification
-of the program output is unambiguous, so all programs that
-one can synthesize compute the same results for all inputs.
-
-Remarks on Uniqueness
-^^^^^^^^^^^^^^^^^^^^^
-
-Let us give a name to the specification for `sort2`.
-
-.. code-block:: scala
-
- def sort2spec(x: BigInt, y: BigInt, res: (BigInt, BigInt)): Boolean = {
- Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
- }
-
-We can then prove that the result is unique, by asking Leon
-to show the following function returns `true` for all inputs
-for which the `require` clause holds.
-
-.. code-block:: scala
-
- def unique2(x: BigInt, y: BigInt,
- res1: (BigInt, BigInt),
- res2: (BigInt, BigInt)): Boolean = {
- require(sort2spec(x,y,res1) && sort2spec(x,y,res2))
- res1 == res2
- }.holds
-
-In contrast, if we define the corresponding specification for three integers
-
-.. code-block:: scala
-
- def sort3spec(x: BigInt, y: BigInt, z: BigInt, res: (BigInt, BigInt, BigInt)): Boolean = {
- Set(x,y,z) == Set(res._1, res._2, res._3) &&
- res._1 <= res._2 && res._2 <= res._3
- }
-
-Then uniqueness of the solution is the following conjecture:
-
-.. code-block:: scala
-
- def unique3(x: BigInt, y: BigInt, z: BigInt,
- res1: (BigInt, BigInt, BigInt),
- res2: (BigInt, BigInt, BigInt)): Boolean = {
- require(sort3spec(x,y,z,res1) && sort3spec(x,y,z,res2))
- res1 == res2
- }.holds
-
-This time, however, Leon will report a counterexample, indicating
-that the conjecture does not hold. One such counterexample is
-0, 1, 1, for which the result (0, 0, 1) also satisfies the specification,
-because sets ignore the duplicates, so
-
-.. code-block:: scala
-
- Set(x,y,z) == Set(res._1, res._2, res._2)
-
-is true. This shows that writing specifications can be subtle, but Leon's
-capabilities can help in the process as well.
-
-**Question:** Write the specification that requires the output triple
-to be strictly sorted using the `<` relation. Use `choose` to define
-the corresponding `sort3` function.
-Try executing such
-specifications for example inputs. What happens if you execute it
-when two of the elements are equal? Write the `require` clause
-to enforce the precondition that the initial elements are distinct.
-Formulate in Leon the statement
-that for triples of distinct elements the result of strictly ordering
-them is unique and try to prove it.
-
-Interactive Exploration of Program Space
-----------------------------------------
-
-For larger programs, the search may take too long to find
-the solution and Leon will time out. In such cases, instead
-of invoking automated search, you can invoke Leon in the
-mode where the user directs each synthesis step to be
-provided. This is a great way to understand the rules that
-Leon currently has available for performing synthesis.
-
-In the `web interface`, select on the synthesis task for
-`sort2` specification using the `choose` construct and
-select `Explore` instead of the automated `Search`. You can
-then navigate the space of programs interactively. Select
-the `Inequality split` between the two input variables. The
-system will apply this inference rule, and transform the
-program with one `choose` into a program that performs case
-analysis and then performs `choose` in each branch. For
-individual branches we can try to resolve them using the
-`CEGIS` synthesis rule, which searches for small expressions
-and tries to find the one that satisfies the specification.
-We can use `Equivalent Inputs` and `Unused Inputs` as
-needed, since they are generally a good idea to apply. Once
-all sub-goals are resolved, select `Import Code`. Note
-that you can import any of the intermediate steps in exploration:
-the program with `choose` is valid in Leon, and it can even
-be executed, thanks to run-time constraint solving for the
-cases containing `choose`.
-
-**Question:** Use interactive exploration to synthesize
-`sort3` function by performing inequality splits in the
-interactive interface. Given three variables, you will
-need to perform inequality splits on their pairs until
-the tuple to be returned is known thanks to the tests
-performed in the code. This is a somewhat tedious process,
-but relatively easy, and the result is guaranteed to be
-correct.
-
-Defining Lists and Their Properties
------------------------------------
-
-We next consider sorting an unbounded number of elements.
-For this purpose, we define a data structure for lists of
-integers. Leon has a built-in data type of parametric
-lists, see :ref:`Leon Library <library>`, but here we define
-our own variant instead.
-
-Lists
-^^^^^
-
-We use a recursive algebraic data type
-definition, expressed using Scala's **case classes**.
-
-.. code-block:: scala
-
- sealed abstract class List
- case object Nil extends List
- case class Cons(head: BigInt, tail: List) extends List
-
-We can read the definition as follows: the set of lists is
-defined as the least set that satisfies them:
-
- * empty list `Nil` is a list
- * if `head` is an integer and `tail` is a `List`, then
- `Cons(head,tail)` is a `List`.
-
-Each list is constructed by applying the above two rules
-finitely many times. A concrete list containing elements 5,
-2, and 7, in that order, is denoted
-
-.. code-block:: scala
-
- Cons(5, Cons(2, Cons(7, Nil)))
-
-Having defined the structure of lists, we can move on to
-define some semantic properties of lists that are of
-interests. For this purpose, we use recursive functions
-defined on lists.
-
-Size of a List
-^^^^^^^^^^^^^^
-
-As the starting point, we define size of a list.
-
-.. code-block:: scala
-
- def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(x, rest) => 1 + size(rest)
- })
-
-The definition uses *pattern matching* to define size of the
-list in the case it is empty (where it is zero) and when it
-is non-empty, or, if its non-empty, then it has a head `x`
-and the rest of the list `rest`, so the size is one plus the
-size of the rest. Thus `size` is a recursive function. A
-strength of Leon is that it allows using such recursive
-functions in specifications.
-
-It makes little sense to try to write a complete
-specification of `size`, given that its recursive definition
-is already a pretty clear description of its
-meaning. However, it is useful to add a consequence of this
-definition, namely that the size is non-negative. The reason
-is that Leon most of the time reasons by unfolding `size`,
-and the property of size being non-negative is not revealed
-by such unfolding. Once specified, the non-negativity is
-easily proven and Leon will make use of it.
-
-.. code-block:: scala
-
- def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(x, rest) => 1 + size(rest)
- }) ensuring(res => res >= 0)
-
-
-Sorted Lists
-^^^^^^^^^^^^
-
-We define properties of values simply as executable
-predicates that check if the property holds. The following
-is a property that a list is sorted in a strictly ascending
-order.
-
-.. code-block:: scala
-
- def isSorted(l : List) : Boolean = l match {
- case Nil => true
- case Cons(_,Nil) => true
- case Cons(x1, Cons(x2, rest)) =>
- x1 < x2 && isSorted(Cons(x2,rest))
- }
-
-Insertion into Sorted List
---------------------------
-
-Consider the following specification of insertion into a sorted list,
-which is a building block for an insertion sort.
-
-.. code-block:: scala
-
- def sInsert(x : BigInt, l : List) : List = {
- require(isSorted(l))
- l match {
- case Nil => Cons(x, Nil)
- case Cons(e, rest) if (x == e) => l
- case Cons(e, rest) if (x < e) => Cons(x, Cons(e,rest))
- case Cons(e, rest) if (x > e) => Cons(e, sInsert(x,rest))
- }
- } ensuring {(res:List) => isSorted(res)}
-
-Leon verifies that the returned list is indeed sorted. Note
-how we are again using a recursively defined function to
-specify another function. We can introduce a bug into the
-definition above and examine the counterexamples that Leon
-finds.
-
-Being Sorted is Not Enough
---------------------------
-
-Note, however, that a function such as this one is also correct.
-
-.. code-block:: scala
-
- def fsInsert(x : BigInt, l : List) : List = {
- require(isSorted(l))
- Nil
- } ensuring {(res:List) => isSorted(res)}
-
-So, our specification may be considered weak, because it does
-not say anything about the elements.
-
-Using Size in Specification
----------------------------
-
-Consider a stronger additional postcondition property:
-
-.. code-block:: scala
-
- size(res) == size(l) + 1
-
-Does it hold? If we try to add it, we obtain a counterexample.
-A correct strengthening, taking into account that the element
-may or may not already be in the list, is the following.
-
-.. code-block:: scala
-
- size(l) <= size(res) && size(res) <= size(l) + 1
-
-Using Content in Specification
-------------------------------
-
-A stronger specification needs to talk about the `content`
-of the list.
-
-.. code-block:: scala
-
- def sInsert(x : BigInt, l : List) : List = {
- require(isSorted(l))
- l match {
- case Nil => Cons(x, Nil)
- case Cons(e, rest) if (x == e) => l
- case Cons(e, rest) if (x < e) => Cons(x, Cons(e,rest))
- case Cons(e, rest) if (x > e) => Cons(e, sInsert(x,rest))
- }
- } ensuring {(res:List) =>
- isSorted(res) && content(res) == content(l) ++ Set(x)}
-
-To compute `content`, in this example we use sets (even
-though in general it might be better in general to use bags
-i.e. multisets).
-
-.. code-block:: scala
-
- def content(l: List): Set[BigInt] = l match {
- case Nil => Set()
- case Cons(i, t) => Set(i) ++ content(t)
- }
-
-
-Sorting Specification and Running It
-------------------------------------
-
-Specifying sorting is in fact very easy.
-
-.. code-block:: scala
-
- def sortMagic(l : List) = {
- ???[List]
- } ensuring((res:List) =>
- isSorted(res) && content(res) == content(l))
-
-We can execute such a sort.
-
-.. code-block:: scala
-
- def mm = sortMagic(Cons(20, Cons(5, Cons(50, Cons(2, Nil)))))
-
-obtaining the expected `Cons(2, Cons(5, Cons(20, Cons(50, Nil))))`.
-Note that the function actually removes duplicates from the input list.
-
-Synthesizing Sort
------------------
-
-By asking the system to synthesize the `choose` construct inside `magicSort`,
-we may obtain a function such as the following, which gives
-us the natural insertion sort.
-
-.. code-block:: scala
-
- def sortMagic(l : List): List = {
- l match {
- case Cons(head, tail) =>
- sInsert(head, sortMagic(tail))
- case Nil => Nil
- }
- }
-
-Going back and Synthesizing Insertion
--------------------------------------
-
-In fact, if we have a reasonably precise enough
-specification of insert, we can synthesize the implementation.
-To try this, remove the body of `sInsert` and replace it
-with `???[List]` denoting an unknown value of the given type.
-
-.. code-block:: scala
-
- def sInsert(x : BigInt, l : List) : List = {
- require(isSorted(l))
- ???[List]
- } ensuring {(res:List) =>
- isSorted(res) && content(res) == content(l) ++ Set(x)}
-
-Leon can then synthesize the missing part, resulting in a similar
-body to the one we wrote by hand originally.
-
-Repairing an Incorrect Function
--------------------------------
-
-You may notice that synthesis can take a long time and fail.
-Often we do produce some version of the program, but it is
-not correct according to a specification. Consider the
-following attempt at `sInsert`.
-
-.. code-block:: scala
-
- def sInsert(x : BigInt, l : List) : List = {
- require(isSorted(l))
- l match {
- case Nil => Cons(x, Nil)
- case Cons(e, rest) => Cons(e, sInsert(x,rest))
- }
- } ensuring {(res:List) =>
- isSorted(res) && content(res) == content(l) ++ Set(x)}
-
-Leon reports a counterexample to the correctness. Instead of
-trying to manually understand the counterexample, we can
-instruct the system to **repair** this solution. If Leon can
-reuse parts of the existing function, it can be much faster
-than doing synthesis from scratch. Leon automatically finds
-test inputs that it uses to localize the error and preserve
-useful existing pieces of code. In this case, Leon repairs
-the above function into the one equivalent to the original
-one, by doing a case split and synthesizing two new cases,
-resulting in the following equivalent function.
-
-.. code-block:: scala
-
- def sInsert(x : BigInt, l : List): List = {
- require(isSorted(l))
- l match {
- case Nil => Cons(x, Nil)
- case Cons(e, rest) =>
- if (x < e) Cons(x, l)
- else if (x == e) Cons(x, rest)
- else Cons(e, sInsert(x, rest))
- } ensuring { (res : List) =>
- isSorted(res) && content(res) == content(l) ++ Set[BigInt](x) }
-
-
-This completes the tutorial. To learn more, check the rest of this documentation and browse the examples provided with Leon.
diff --git a/src/sphinx/verification.rst b/src/sphinx/verification.rst
deleted file mode 100644
index b8af549751c717d48f1b3d4af43a422ef109d26b..0000000000000000000000000000000000000000
--- a/src/sphinx/verification.rst
+++ /dev/null
@@ -1,231 +0,0 @@
-.. _verification:
-
-Verification
-============
-
-Software verification aims at making software safer. In its typical use case,
-it is a tool that takes as input the source code of a program with
-specifications as annotations and attempt to prove --- or disprove --- their
-validity.
-
-One of the core module of Leon is a verifier for the subset of Scala described
-in the sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`. In this
-section we describe the specification language that can be used to declare
-properties of programs, as well as the safety properties automatically checked
-by Leon. We also discuss how Leon can be used to prove mathematical theorems.
-
-Verification conditions
------------------------
-
-Given an input program, Leon generates individual verification conditions
-corresponding to different properties of the program. A program is correct if
-all of the generated verification conditions are ``valid``. The validity of some
-conditions depends on the validity of other conditions --- typically a
-postcondition is ``valid`` assuming the precondition is ``valid``.
-
-For each function, Leon attempts to verify its contract, if there is one. A
-*contract* is the combination of a *precondition* and a *postcondition*. A
-function meets its contract if for any input parameter that passes the
-precondition, the postcondition holds after executing the function.
-Preconditions and postconditions are annotations given by the user --- they are
-the specifications and hence cannot be inferred by a tool and must be provided.
-
-In addition to user-provided contracts, Leon will also generate a few safety
-verification conditions of its own. It will check that all of the array
-accesses are within proper bounds, and that pattern matching always covers all
-possible cases, even given complex precondition. The latter is different from
-the Scala compiler checks on pattern matching exhaustiveness, as Leon considers
-information provided by (explicit or implicit) preconditions to the ``match``
-expression.
-
-Postconditions
-**************
-
-One core concept in verification is to check the contract of functions. The most
-important part in a contract is the postcondition. The postcondition specifies
-the behaviour of the function. It takes into account the precondition and only
-asserts the property of the output when the input satisfies the precondition.
-
-Formally, we consider a function with a single parameter (one can generalize
-the following for any number of parameters):
-
-.. code-block:: scala
-
- def f(x: A): B = {
- require(prec)
- body
- } ensuring(r => post)
-
-where, :math:`\mbox{prec}(x)` is a Boolean expression with free variables
-contained in :math:`\{ x \}`, :math:`\mbox{body}(x)` is an expression with
-free variables contained in :math:`\{ x \}` and :math:`\mbox{post}(x, r)` is a
-Boolean expression with free variables contained in :math:`\{ x, r \}`. The
-types of :math:`x` and :math:`r` are respectively ``A`` and ``B``. We write
-:math:`\mbox{expr}(a)` to mean the substitution in :math:`\mbox{expr}` of its
-free variable by :math:`a`.
-
-Leon attempts to prove the following theorem:
-
-.. math::
-
- \forall x. \mbox{prec}(x) \implies \mbox{post}(x, \mbox{body}(x))
-
-If Leon is able to prove the above theorem, it returns ``valid`` for the
-function ``f``. This gives you a guarantee that the function ``f`` is correct
-with respect to its contract.
-
-However, if the theorem is not valid, Leon will return a counterexample to the
-theorem. The negation of the theorem is:
-
-.. math::
-
- \exists x. \mbox{prec}(x) \land \neg \mbox{post}(x, \mbox{body}(x))
-
-and to prove the validity of the negation, Leon finds a witness :math:`x` --- a
-counterexample --- such that the precondition is verified and the postcondition
-is not.
-
-The general problem of verification is undecidable for a Turing-complete
-language, and the Leon language is Turing-complete. So Leon has to be
-incomplete in some sense. Generally, Leon will eventually find a counterexample
-if one exists. However, in practice some program structures require too many
-unrollings and Leon is likely to timeout (or being out of memory) before
-finding the counterexample. When the postcondition is valid, it could also
-happen that Leon keeps unrolling the program forever, without being able to
-prove the correctness. We discuss the exact conditions for this in the
-chapter on Leon's algorithms.
-
-Preconditions
-*************
-
-Preconditions are used as part of the contract of functions. They are a way to
-restrict the input to only relevant inputs, without having to implement guards
-and error handling in the functions themselves.
-
-Preconditions are contracts that the call sites should respect, and thus are
-not checked as part of verifying the function. Given the following definition:
-
-.. code-block:: scala
-
- def f(x: A): B = {
- require(prec)
- body
- }
-
-
-For each call site in the whole program (including in ``f`` itself):
-
-.. code-block:: scala
-
- ...
- f(e)
- ...
-
-where the expression :math:`\mbox{e}(x)` is an expression of type ``A`` with
-free variables among :math:`\{ x \}`. Let us define the path condition on :math:`x`
-at that program point as :math:`\mbox{pc}(x)`. The path condition is a formula that
-summarizes the facts known about :math:`x` at that call site. A typical example is
-when the call site is inside an if expression:
-
-.. code-block:: scala
-
- if(x > 0)
- f(x)
-
-The path condition on :math:`x` would include the fact that :math:`x > 0`. This
-path condition is then used as a precondition of proving the validity of the
-call to :math:`\mbox{f}`. Formally, for each such call site, Leon will attempt
-to prove the following theorem:
-
-.. math::
-
- \forall x. \mbox{pc}(x) \implies \mbox{prec}(\mbox{e}(x))
-
-Leon will generates one such theorem for each static call site of a function with
-a precondition.
-
-.. note::
-
- Leon only assumes an open program model, where any function could be called from
- outside of the given program. In particular, Leon will not derive a precondition
- to a function based on known information in the context of the calls, such as
- knowing that the function is always given positive parameters. Any information needed
- to prove the postcondition will have to be provide as part of the precondition
- of a function.
-
-Loop invariants
-***************
-
-Leon supports annotations for loop invariants in :ref:`XLang <xlang>`. To
-simplify the presentation we will assume a single variable :math:`x` is in
-scope, but the definitions generalize to any number of variables. Given the
-following program:
-
-.. code-block:: scala
-
- (while(cond) {
- body
- }) invariant(inv)
-
-where the Boolean expression :math:`\mbox{cond}(x)` is over the free variable
-:math:`x` and the expression :math:`\mbox{body}(x, x')` relates the value of
-:math:`x` when entering the loop to its updated value :math:`x'` on loop exit.
-The expression :math:`\mbox{inv}(x)` is a Boolean formula over the free
-variable :math:`x`.
-
-A loop invariant must hold:
- (1) when the program enters the loop initially
- (2) after each completion of the body
- (3) right after exiting the loop (when the condition turns false)
-
-Leon will prove point (1) and (2) above. Together, and by induction, they imply
-that point (3) holds as well.
-
-Array access safety
-*******************
-
-Leon generates verification conditions for the safety of array accesses. For
-each array variable, Leon carries along a symbolic information on its length.
-This information is used to prove that each expression used as an index in the
-array is strictly smaller than that length. The expression is also checked to
-be positive.
-
-Pattern matching exhaustiveness
-*******************************
-
-Leon verifies that pattern matching is exhaustive. The regular Scala compiler
-only considers the types of expression involved in pattern matching, but Leon
-will consider information such as precondition to formally prove the
-exhaustiveness of pattern matching.
-
-As an example, the following code should issue a warning with Scala:
-
-.. code-block:: scala
-
- abstract class List
- case class Cons(head: Int, tail: List) extends List
- case object Nil extends List
-
- def getHead(l: List): Int = {
- require(!l.isInstanceOf[Nil])
- l match {
- case Cons(x, _) => x
- }
- }
-
-But Leon will prove that the pattern matching is actually exhaustive,
-relying on the given precondition.
-
-Pretty-printing
----------------
-
-If a global function name ends with "``toString``" with any case, has only one argument and returns a string, this function will be used when printing verification examples. This function can be synthesized (see the synthesis section). For example,
-
-.. code-block:: scala
-
- def intToString(i: Int) = "#" + i.toString + ",..."
- def allIntsAreLessThan9(i: Int) = i <= 9 holds
-
-It will display the counter example for ``allIntsAreLessThan9`` as:
-
- Counter-example: ``#10,...``
diff --git a/src/sphinx/xlang.rst b/src/sphinx/xlang.rst
deleted file mode 100644
index d2eace3b9120397fcc3bcad70ca79bc167593e23..0000000000000000000000000000000000000000
--- a/src/sphinx/xlang.rst
+++ /dev/null
@@ -1,246 +0,0 @@
-.. _xlang:
-
-XLang
-=====
-
-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.
-
-On the technical side, these extensions do not have specific treatment in the
-back-end of Leon. Instead, they are desugared into :ref:`Pure Scala <purescala>`
-constructs during a preprocessing phase in the Leon front-end.
-
-Imperative Code
----------------
-
-XLang lets you introduce local variables in functions, and use Scala assignments
-syntax.
-
-.. code-block:: scala
-
- def foo(x: Int): Int = {
- var a = x
- var b = 42
- a = a + b
- b = a
- b
- }
-
-The above example illustrates three new features introduced by XLang:
-
-1. Declaring a variable in a local scope
-
-2. Blocks of expressions
-
-3. Assignments
-
-You can use Scala variables with a few restrictions. The variables can only be
-declared and used locally, no variable declaration outside of a function body.
-There is also support for variables in case classes constructors. XLang
-introduces the possibility to use sequences of 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.
-
-
-While loops
------------
-
-You can use the ``while`` keyword. While loops usually combine the ability to
-declare variables and make a sequence of assignments in order to compute
-something useful:
-
-.. code-block:: scala
-
- def foo(x: Int): Int = {
- var res = 0
- var i = 0
- while(i < 10) {
- res = res + i
- i = i + 1
- }
- res
- }
-
-Leon will automatically generate a postcondition to the ``while`` loop, using
-the negation of the loop condition. It will automatically prove that
-verification condition and you should see an ``invariant postcondition`` marked
-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. Usually that invariant is too weak to prove anything remotely
-useful and you will need to annotate the loop with a stronger invariant.
-
-You can annotate 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.
-
-.. 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
-
- val a = Array(1,2,3,4)
- a(1) //2
- a(1) = 10
- a(1) //10
-
-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.
-
-Mutable Objects
----------------
-
-A restricted form of mutable classes is supported via case classes with ``var``
-arguments:
-
-.. code-block:: scala
-
- case class A(var x: Int)
- def f(): Int = {
- val a = new A(10)
- a.x = 13
- a.x
- }
-
-Mutable case classes are behaving similarly to ``Array``, and are handled with a
-rewriting, where each field updates becomes essentially a copy of the object with
-the modified parameter changed.
-
-Aliasing
---------
-
-With mutable data structures comes the problem of aliasing. In Leon, we
-maintain the invariant that in any scope, there is at most one pointer to some
-mutable structure. Leon will issue an error if you try to create an alias to
-some mutable structure in the same scope:
-
-.. code-block:: scala
-
- val a = Array(1,2,3,4)
- val b = a //error: illegal aliasing
- b(0) = 10
- assert(a(0) == 10)
-
-However, Leon correctly supports aliasing mutable structures when passing it
-as a parameter to a function (assuming its scope is not shared with the call
-site, i.e. not a nested function). Essentially you can do:
-
-.. code-block:: scala
-
- case class A(var x: Int)
- def updateA(a: A): Unit = {
- a.x = 14
- }
- def f(): Unit = {
- val a = A(10)
- updateA(a)
- assert(a.x == 14)
- }
-
-The function ``updateA`` will have the side effect of updating its argument
-``a`` and this will be visible at the call site.
-
-Annotations for Imperative Programming
---------------------------------------
-
-XLang introduces the special function ``old`` that can be used in postconditions to
-talk about the value of a variable before the execution of the block. When you refer to a variable
-or mutable structure in a post-condition, leon will always consider the current value of
-the object, so that in the case of a post-condition this would refer to the final value of the
-object. Using ``old``, you can refer to the original value of the variable and check some
-properties:
-
-.. code-block:: scala
-
- case class A(var x: Int)
- def inc(a: A): Unit = {
- a.x = a.x + 1
- } ensuring(_ => a.x == old(a).x + 1)
-
-``old`` can be wrapped around any identifier that is affected by the body. You can also use
-``old`` for variables in scope, in case of nested functions:
-
-.. code-block:: scala
-
- def f(): Int = {
- var x = 0
- def inc(): Unit = {
- x = x + 1
- } ensuring(_ => x == old(x) + 1)
-
- inc(); inc();
- assert(x == 2)
- }
-
-
-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.