jyapayne/Nim
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Improve Markdown code blocks & start moving docs to Markdown style (#19954)

Browse source 
- add additional parameters parsing (other implementations will just
  ignore them). E.g. if in RST we have:

  .. code:: nim
     :test: "nim c $1"

     ...

  then in Markdown that will be:

  ```nim test="nim c $1"
  ...
  ```

- implement Markdown interpretation of additional indentation which is
  less than 4 spaces (>=4 spaces is a code block but it's not
implemented yet). RST interpretes it as quoted block, for Markdown it's
just normal paragraphs.
- add separate `md2html` and `md2tex` commands. This is to separate
  Markdown behavior in cases when it diverges w.r.t. RST significantly —
most conspicously like in the case of additional indentation above, and
also currently the contradicting inline rule of Markdown is also turned
on only in `md2html` and `md2tex`. **Rationale:** mixing Markdown and
RST arbitrarily is a way to nowhere, we need to provide a way to fix the
particular behavior. Note that still all commands have **both** Markdown
and RST features **enabled**. In this PR `*.nim` files can be processed
only in Markdown mode, while `md2html` is for `*.md` files and
`rst2html` for `*.rst` files.
- rename `*.rst` files to `.*md` as our current default behavior is
  already Markdown-ish
- convert code blocks in `docgen.rst` to Markdown style as an example.
  Other code blocks will be converted in the follow-up PRs
- fix indentation inside Markdown code blocks — additional indentation
  is preserved there
- allow more than 3 backticks open/close blocks (tildas \~ are still not
  allowed to avoid conflict with RST adornment headings) see also
https://github.com/nim-lang/RFCs/issues/355
- better error messages
- (other) fix a bug that admonitions cannot be used in sandbox mode; fix
  annoying warning on line 2711
This commit is contained in:
Andrey Makarov 2022-07-15 20:27:54 +03:00 • committed by GitHub
commit 417b90a7e5
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
47 changed files with 341 additions and 126 deletions
Download patch file Download diff file Expand all files Collapse all files

205
doc/drnim.rst
View file

@ -1,205 +0,0 @@
===================================
DrNim User Guide
===================================
:Author: Andreas Rumpf
:Version: |nimversion|
.. default-role:: code
.. include:: rstcommon.rst
.. contents::
Introduction
============
This document describes the usage of the *DrNim* tool. DrNim combines
the Nim frontend with the `Z3 <https://github.com/Z3Prover/z3>`_ proof
engine, in order to allow verify/validate software written in Nim.
DrNim's command-line options are the same as the Nim compiler's.
DrNim currently only checks the sections of your code that are marked
via `staticBoundChecks: on`:
.. code-block:: nim
{.push staticBoundChecks: on.}
# <--- code section here ---->
{.pop.}
DrNim currently only tries to prove array indexing or subrange checks,
overflow errors are *not* prevented. Overflows will be checked for in
the future.
Later versions of the **Nim compiler** will **assume** that the checks inside
the `staticBoundChecks: on` environment have been proven correct and so
it will **omit** the runtime checks. If you do not want this behavior, use
instead `{.push staticBoundChecks: defined(nimDrNim).}`. This way the
Nim compiler remains unaware of the performed proofs but DrNim will prove
your code.
Installation
============
Run `koch drnim`:cmd:, the executable will afterwards be
in ``$nim/bin/drnim``.
Motivating Example
==================
The follow example highlights what DrNim can easily do, even
without additional annotations:
.. code-block:: nim
{.push staticBoundChecks: on.}
proc sum(a: openArray[int]): int =
for i in 0..a.len:
result += a[i]
{.pop.}
echo sum([1, 2, 3])
This program contains a famous "index out of bounds" bug. DrNim
detects it and produces the following error message::
cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
In other words for `i == 0` and `a.len == 0` (for example!) there would be
an index out of bounds error.
Pre-, postconditions and invariants
===================================
DrNim adds 4 additional annotations (pragmas) to Nim:
- `requires`:idx:
- `ensures`:idx:
- `invariant`:idx:
- `assume`:idx:
These pragmas are ignored by the Nim compiler so that they don't have to
be disabled via `when defined(nimDrNim)`.
Invariant
---------
An `invariant` is a proposition that must be true after every loop
iteration, it's tied to the loop body it's part of.
Requires
--------
A `requires` annotation describes what the function expects to be true
before it's called so that it can perform its operation. A `requires`
annotation is also called a `precondition`:idx:.
Ensures
-------
An `ensures` annotation describes what will be true after the function
call. An `ensures` annotation is also called a `postcondition`:idx:.
Assume
------
An `assume` annotation describes what DrNim should **assume** to be true
in this section of the program. It is an unsafe escape mechanism comparable
to Nim's `cast` statement. Use it only when you really know better
than DrNim. You should add a comment to a paper that proves the proposition
you assume.
Example: insertionSort
======================
**Note**: This example does not yet work with DrNim.
.. code-block:: nim
import std / logic
proc insertionSort(a: var openArray[int]) {.
ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
for k in 1 ..< a.len:
{.invariant: 1 <= k and k <= a.len.}
{.invariant: forall(j in 1..<k, i in 0..<j, a[i] <= a[j]).}
var t = k
while t > 0 and a[t-1] > a[t]:
{.invariant: k < a.len.}
{.invariant: 0 <= t and t <= k.}
{.invariant: forall(j in 1..k, i in 0..<j, j == t or a[i] <= a[j]).}
swap a[t], a[t-1]
dec t
Unfortunately, the invariants required to prove that this code is correct take more
code than the imperative instructions. However, this effort can be compensated
by the fact that the result needs very little testing. Be aware though that
DrNim only proves that after `insertionSort` this condition holds::
forall(i in 1..<a.len, a[i-1] <= a[i])
This is required, but not sufficient to describe that a `sort` operation
was performed. For example, the same postcondition is true for this proc
which doesn't sort at all:
.. code-block:: nim
import std / logic
proc insertionSort(a: var openArray[int]) {.
ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
# does not sort, overwrites `a`'s contents!
for i in 0..<a.len: a[i] = i
Syntax of propositions
======================
The basic syntax is `ensures|requires|invariant: <prop>`.
A `prop` is either a comparison or a compound::
prop = nim_bool_expression
| prop 'and' prop
| prop 'or' prop
| prop '->' prop # implication
| prop '<->' prop
| 'not' prop
| '(' prop ')' # you can group props via ()
| forallProp
| existsProp
forallProp = 'forall' '(' quantifierList ',' prop ')'
existsProp = 'exists' '(' quantifierList ',' prop ')'
quantifierList = quantifier (',' quantifier)*
quantifier = <new identifier> 'in' nim_iteration_expression
`nim_iteration_expression` here is an ordinary expression of Nim code
that describes an iteration space, for example `1..4` or `1..<a.len`.
`nim_bool_expression` here is an ordinary expression of Nim code of
type `bool` like `a == 3` or `23 > a.len`.
The supported subset of Nim code that can be used in these expressions
is currently underspecified but `let` variables, function parameters
and `result` (which represents the function's final result) are amenable
for verification. The expressions must not have any side-effects and must
terminate.
The operators `forall`, `exists`, `->`, `<->` have to imported
from `std / logic`.