structure of verification chapter

doc/verification.rst

 Verification
 ============
+
+Software verification aims at making software safer. In its typical use case,
+it is a tool that takes as input the source code of a program with
+specifications as annotations and attempt to prove --- or disprove --- their
+validity.
+
+One of the core module of Leon is a verifier for the subset of Scala described
+in the sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`. In this
+section we describe the specification language that can be used to declare
+properties of programs, as well as the safety properties automatically checked
+by Leon. We also discuss how Leon can be used to prove mathematical theorems.
+
+Verification conditions
+-----------------------
+
+
+
+Postconditions
+**************
+
+
+Preconditions
+*************
+
+
+Loop invariants
+***************
+
+
+Array access safety
+*******************
+
+
+Pattern matching exhaustiveness
+*******************************
+
+
+
+Proving mathematical theorems with Leon
+---------------------------------------