loop invariants

doc/verification.rst

+.. _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
 *******************