diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst index ea6843fdee2421ab8a4a557108fffcf815662e93..2e5576d1df3f80eefc9fd97cc12dba1491b23d16 100644 --- a/doc/gettingstarted.rst +++ b/doc/gettingstarted.rst @@ -97,7 +97,7 @@ be used directly from the shell, see 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 +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/doc/installation.rst b/doc/installation.rst index 01c0b680083490e52bd24176a84068f286330aa3..da3a2d18ffab672a097f62cb4f92d39ae9265f57 100644 --- a/doc/installation.rst +++ b/doc/installation.rst @@ -5,7 +5,7 @@ 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 -much easier to build on Unix-like plattforms. Not to say it is impossible to +much easier to build on Unix-like platforms. Not to say it is impossible to build on Windows. But some scripts used to run and test the system are shell script and you will need to manually port them to Windows if you wish to use Windows. @@ -33,7 +33,7 @@ Get the sources of Leon by cloning the official Leon repository: $ sbt clean compile // takes about 3 minutes -We now use ``sbt script`` to create a ``leon`` bash script that runs leon with +We now use ``sbt script`` to create a ``leon`` bash script that runs Leon with all the appropriate settings: .. code-block:: bash @@ -97,8 +97,8 @@ In any case, we recommend that you install both solvers separately and have their binaries available in the ``$PATH``. Since the default solver uses the native Z3 API, you will have to explicitly -specify another solver if this native layer is not available to you. Check also the -the ``--solvers`` in :ref:`cmdlineoptions` . +specify another solver if this native layer is not available to you. Check also +the ``--solvers`` option in :ref:`cmdlineoptions` . Building Documentation ---------------------- diff --git a/doc/intro.rst b/doc/intro.rst index 0744521968e8e21eedec612f24f60539cd7fc28e..0340073161245d36d2f86191927103319ca38441 100644 --- a/doc/intro.rst +++ b/doc/intro.rst @@ -55,13 +55,13 @@ 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 satisfiying the precondition, the postcondition will always hold. + 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 occuring in the external + 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 diff --git a/doc/library.rst b/doc/library.rst index a165c0a6b0976f90e35802181f7fe433c7abef32..bb84c9b94c80ca1cddd1c7c8275b22b771f10cd9 100644 --- a/doc/library.rst +++ b/doc/library.rst @@ -227,13 +227,13 @@ The object ``ListOps`` offers this additional operations: | | formed by the elements of these Lists. | +--------------------------------------------------------+---------------------------------------------------+ | ``isSorted(ls: List[BigInt]): Boolean`` | Returns whether this list of mathematical integers| -| | is sorted in accending order. | +| | is sorted in ascending order. | +--------------------------------------------------------+---------------------------------------------------+ | ``sorted(ls: List[BigInt]): List[BigInt]`` | Sorts this list of mathematical integers | -| | is sorted in accending order. | +| | is sorted in ascending order. | +--------------------------------------------------------+---------------------------------------------------+ | ``insSort(ls: List[BigInt], v: BigInt): List[BigInt]`` | Sorts this list of mathematical integers | -| | is sorted in accending order using insertion sort.| +| | is sorted in ascending order using insertion sort.| +--------------------------------------------------------+---------------------------------------------------+ Theorems on Lists diff --git a/doc/options.rst b/doc/options.rst index 02f990fb3a35913beafe0993d29145b42901f100..09f31a1e21f37a363867ecc9cc447fa8ecf17e96 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -205,7 +205,7 @@ These options are also used by repair during the synthesis stage. * ``--cegis:shrink`` - Shrink non-det programs when tests pruning works well. + Shrink non-deterministic programs when tests pruning works well. * ``--cegis:vanuatoo`` diff --git a/doc/repair.rst b/doc/repair.rst index 0081395f382121d28642aa8ac2cc463c91ad692b..614f829d002dab76381a28c7d382262ad2daace5 100644 --- a/doc/repair.rst +++ b/doc/repair.rst @@ -99,7 +99,7 @@ Fault Localization ****************** In the next step, Leon will try to localize the problem to the smallest -possible subexression of the function body. The idea is to run the failing +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 diff --git a/doc/verification.rst b/doc/verification.rst index e19b1168f090675236e505ac4f1253cb5af76606..8778e31d841285f0ad177561a77304b57fdb73c4 100644 --- a/doc/verification.rst +++ b/doc/verification.rst @@ -28,7 +28,7 @@ For each function, Leon attempts to verify its contract, if there is one. 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 secifications and hence cannot be infered by a tool and must be provided. +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 diff --git a/doc/xlang.rst b/doc/xlang.rst index b3236443fbfebcce48c31c71612feff83090674b..3f88e3e26386064efd82ce4f881164b126d8309b 100644 --- a/doc/xlang.rst +++ b/doc/xlang.rst @@ -10,10 +10,9 @@ 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. -Technically, these extensions are implemented using a translation to :ref:`Pure -Scala <purescala>`. This means They are not implemented in the back-end -solving system of Leon, but parsed in the the front-end and eliminated early -during the Leon pipelining process. +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 --------------- @@ -94,9 +93,9 @@ 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 anotate the loop with a stronger invariant. +useful and you will need to annotate the loop with a stronger invariant. -You can anotate a loop with an invariant as follows: +You can annotate a loop with an invariant as follows: .. code-block:: scala