From 692c1524db49de4a2635c313ba3b87f6c5ae97b1 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 24 Apr 2015 20:10:32 +0200
Subject: [PATCH] loop invariants
---
doc/verification.rst | 37 +++++++++++++++++++++++++++++++++++++
1 file changed, 37 insertions(+)
diff --git a/doc/verification.rst b/doc/verification.rst
index 491a26d08..7e1ee7684 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -1,3 +1,5 @@
+.. _verification:
+
Verification
============
@@ -139,10 +141,45 @@ to prove the following theorem:
\forall x. \mbox{pc}(x) \implies \mbox{prec}(\mbox{e}(x))
+Leon will generates one such theorem for each static call site of a function with
+a precondition.
+
+.. note::
+
+ Leon only assumes an open program model, where any function could be called from
+ outside of the given program. In particular, Leon will not derive a precondition
+ to a function based on known information in the context of the calls, such as
+ knowing that the function is always given positive parameters. Any information needed
+ to prove the postcondition will have to be provide as part of the precondition
+ of a function.
Loop invariants
***************
+Leon supports annotations for loop invariants in :ref:`XLang <xlang>`. To
+simplify the presentation we will assume a single variable :math:`x` is in
+scope, but the definitions generalize to any number of variables. Given the
+following program:
+
+.. code-block:: scala
+
+ (while(cond) {
+ body
+ }) invariant(inv)
+
+where the boolean expression :math:`\mbox{cond}(x)` is over the free variable
+:math:`x` and the expression :math:`\mbox{body}(x, x')` relates the value of
+:math:`x` when entering the loop to its updated value :math:`x'` on loop exit.
+The expression :math:`\mbox{inv}(x)` is a boolean formula over the free
+variable :math:`x`.
+
+A loop invariant must hold:
+ (1) when the program enters the loop initially
+ (2) after each completion of the body
+ (3) right after exiting the loop (when the condition turns false)
+
+Leon will prove point (1) and (2) above. Together, and by induction, they imply
+that point (3) holds as well.
Array access safety
*******************
--
GitLab