From dec6efbc731feda2e10768ec6207e2b2f9e66a6e Mon Sep 17 00:00:00 2001 From: Viktor Kuncak <viktor.kuncak@epfl.ch> Date: Fri, 29 May 2015 11:17:47 +0200 Subject: [PATCH] doc: cross references in intro, for impatient. Typo fixed. --- doc/gettingstarted.rst | 2 +- doc/installation.rst | 2 +- doc/intro.rst | 36 ++++++++++++++++++++++++------------ 3 files changed, 26 insertions(+), 14 deletions(-) diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst index 09ddf3543..8e6499550 100644 --- a/doc/gettingstarted.rst +++ b/doc/gettingstarted.rst @@ -30,7 +30,7 @@ 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 predefined examples, +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. diff --git a/doc/installation.rst b/doc/installation.rst index 2b33e83a9..bec009b56 100644 --- a/doc/installation.rst +++ b/doc/installation.rst @@ -96,7 +96,7 @@ Building Documentation To build this documentation locally, you will need Sphinx ( 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`. After installing sphinx, entering the `doc/` directory of diff --git a/doc/intro.rst b/doc/intro.rst index a03c6be0b..c0f572d65 100644 --- a/doc/intro.rst +++ b/doc/intro.rst @@ -1,22 +1,34 @@ Introduction ============ -The Leon system is an automated system for verifying, repairing, and -synthesizing Scala programs. +The Leon system aims to help developers build verified Scala software. +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 -functional subset of Scala. The :ref:`XLang <xlang>` extension enables Leon to -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. +* 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 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 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 -:ref:`XLang <xlang>` can be --- and is --- encoded into a mix of Pure Scala -concepts. However, they are more than just syntactic sugar --- some of those -features actually require significant modification of the original program. +the solving algorithms of Leon. On the other hand, 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. + +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 --------------------- -- GitLab