start formal definition of verification

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:
 
 :: 

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
 *************