From 789ba7ead68eff8aacaa7ad84a8f52973100d066 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 31 Mar 2015 14:45:29 +0200
Subject: [PATCH] introduce verification conditions

---
 doc/verification.rst | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/doc/verification.rst b/doc/verification.rst
index c89ad9136..07582d357 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -15,7 +15,25 @@ by Leon. We also discuss how Leon can be used to prove mathematical theorems.
 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
+conditions depends on the validity of other conditions --- typically a
+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
+function meets its contract if for any input parameter that passes the
+precondition, the postcondition holds after executing the function.
+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.
 
 Postconditions
 **************
-- 
GitLab