Skip to content
Snippets Groups Projects
Commit dec6efbc authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

doc: cross references in intro, for impatient. Typo fixed.

parent f7c8ffaa
No related branches found
No related tags found
No related merge requests found
...@@ -30,7 +30,7 @@ into `y < res`, Leon should report a counterexample; try ...@@ -30,7 +30,7 @@ into `y < res`, Leon should report a counterexample; try
clicking on the names of parameters `x` and `y` as well clicking on the names of parameters `x` and `y` as well
as various parts in the `ensuring` clause. as various parts in the `ensuring` clause.
You can also select from a number of predefined examples, You can also **select from a number of provided examples**,
and then edit them subsequently. Selecting a different and then edit them subsequently. Selecting a different
sample program from the web interface will erase the sample program from the web interface will erase the
previously entered program. previously entered program.
......
...@@ -96,7 +96,7 @@ Building Documentation ...@@ -96,7 +96,7 @@ Building Documentation
To build this documentation locally, you will need Sphinx ( To build this documentation locally, you will need Sphinx (
http://sphinx-doc.org/ ), a restructured text toolkit that http://sphinx-doc.org/ ), a restructured text toolkit that
was originally build to support Python documentation. You will was originally developed to support Python documentation. You will
also need `make`. also need `make`.
After installing sphinx, entering the `doc/` directory of After installing sphinx, entering the `doc/` directory of
......
Introduction Introduction
============ ============
The Leon system is an automated system for verifying, repairing, and The Leon system aims to help developers build verified Scala software.
synthesizing Scala programs. It encourages using a small set of core Scala features, but provides
advanced automation functionality users do not obtain in today's
compilers and development environments for programming languages.
In particular, Leon can
Leon supports programs written in :ref:`Pure Scala <purescala>`, a purely * verify statically that your program confirms to a given
functional subset of Scala. The :ref:`XLang <xlang>` extension enables Leon to specification and that it cannot crash at run-time
work on a richer subset of Scala, including imperative features. From the
perspective of the end user, that distinction between the two sets of features
should be mostly meaningless, but it can help getting an intuition when trying
to prove difficult properties.
* 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 primarily supports programs written in :ref:`Pure Scala <purescala>`, a purely
functional subset of Scala. That said, the :ref:`XLang <xlang>` extension enables Leon to
work on a richer subset of Scala, including imperative features.
The :ref:`Pure Scala <purescala>` features are at the *core* of the Leon 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 system. They are considered as primitives and get a personalized treatment in
the solving algorithms of Leon. On the other hand, any feature introduced by the solving algorithms of Leon. On the other hand, features introduced by
:ref:`XLang <xlang>` can be --- and is --- encoded into a mix of Pure Scala :ref:`XLang <xlang>` are handled by translation into Pure Scala
concepts. However, they are more than just syntactic sugar --- some of those concepts. They are often more than just syntactic sugar, because some of them
features actually require significant modification of the original program. require significant modification of the original program, such as introducing
additional parameters to a set of functions.
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 Software Verification
--------------------- ---------------------
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment