From e6dfce7dff6d8eb479dca590411d61d7ab5ef9f4 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 24 Apr 2015 15:11:27 +0200
Subject: [PATCH] formalize preconditions
---
doc/verification.rst | 46 +++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 45 insertions(+), 1 deletion(-)
diff --git a/doc/verification.rst b/doc/verification.rst
index 67e64be53..491a26d08 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -44,7 +44,8 @@ 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
+Formally, we consider a function with a single parameter (one can generalize
+the following for any number of parameters):
.. code-block:: scala
@@ -95,6 +96,49 @@ chapter on Leon's algorithms.
Preconditions
*************
+Preconditions are used as part of the contract of functions. They are a way to
+restrict the input to only relevant inputs, without having to implement guards
+and error handling in the functions themselves.
+
+Preconditions are contracts that the call sites should respect, and thus are
+not checked as part of verifying the function. Given the following definition:
+
+.. code-block:: scala
+
+ def f(x: A): B = {
+ require(prec)
+ body
+ }
+
+
+For each call site in the whole program (including in ``f`` itself):
+
+.. code-block:: scala
+
+ ...
+ f(e)
+ ...
+
+where the expression :math:`\mbox{e}(x)` is an expression of type ``A`` with
+free variables among :math:`\{ x \}`. Let us define the path condition on :math:`x`
+at that program point as :math:`\mbox{pc}(x)`. The path condition is a formula that
+summarizes the facts known about :math:`x` at that call site. A typical example is
+when the call site is inside an if expression:
+
+.. code-block:: scala
+
+ if(x > 0)
+ f(x)
+
+The path condition on :math:`x` would include the fact that :math:`x > 0`. This
+path condition is then used as a precondition of proving the validity of the
+call to :math:`\mbox{f}`. Formally, for each such call site, Leon will attempt
+to prove the following theorem:
+
+.. math::
+
+ \forall x. \mbox{pc}(x) \implies \mbox{prec}(\mbox{e}(x))
+
Loop invariants
***************
--
GitLab