From 1820ce4f156066669efa7b8d4338e6ca1ef1615e Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 23 Apr 2015 17:40:31 +0200
Subject: [PATCH] start formal definition of verification
---
doc/installation.rst | 2 +-
doc/verification.rst | 37 ++++++++++++++++++++++++++++++-------
2 files changed, 31 insertions(+), 8 deletions(-)
diff --git a/doc/installation.rst b/doc/installation.rst
index 7524221e2..ed9455114 100644
--- a/doc/installation.rst
+++ b/doc/installation.rst
@@ -88,7 +88,7 @@ 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 for you. Check the
+specify another solver if this native layer is not available to you. Check the
the ``--solvers`` command line option:
::
diff --git a/doc/verification.rst b/doc/verification.rst
index 07582d357..a24d4b931 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -17,9 +17,9 @@ 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
+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`.
+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
@@ -29,15 +29,38 @@ 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.
In addition to user-provided contracts, Leon will also generate a few safety
-verification conditions of its own. It will check that any array accesses are
-within proper bounds, and that pattern matching always cover all possible cases,
-even given complex precondition. The latter is different from the Scala compiler
-check on pattern matching exhaustiveness, as Leon considers information provided
-by (explicit or implicit) preconditions to the match expression.
+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
+
+.. code-block:: scala
+
+ def f(x: A): B = {
+ require(prec)
+ body
+ } ensuring(res => post)
+
+where, ``prec`` is a boolean expression with free variables contained in
+``{x}``, and ``post`` is a boolean expression with free variables contained in
+``{x, res}``. The types of ``x`` and ``res`` are respectively ``A`` and ``B``.
+
+Leon attempts to prove the following theorem:
+
+::
+ forall x, prec(x) implies post(body(x), x)
Preconditions
*************
--
GitLab