From 06c1afe2970a2371e0795e4955b497ed751b2448 Mon Sep 17 00:00:00 2001 From: Regis Blanc <regwblanc@gmail.com> Date: Mon, 30 Mar 2015 15:37:40 +0200 Subject: [PATCH] structure of verification chapter --- doc/verification.rst | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/doc/verification.rst b/doc/verification.rst index 0e63a0868..c89ad9136 100644 --- a/doc/verification.rst +++ b/doc/verification.rst @@ -1,2 +1,42 @@ 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 +--------------------------------------- -- GitLab