From fcee8a8722662873a43c1a3896a361fd9f24c9c2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 24 Apr 2015 20:28:53 +0200
Subject: [PATCH] finishing up verification section
---
doc/verification.rst | 26 ++++++++++++++++++++++++++
1 file changed, 26 insertions(+)
diff --git a/doc/verification.rst b/doc/verification.rst
index 7e1ee7684..383292b39 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -184,11 +184,37 @@ that point (3) holds as well.
Array access safety
*******************
+Leon generates verification conditions for the safety of array accesses. For
+each array variable, Leon carries along a symbolic information on its length.
+This information is used to prove that each expression used as an index in the
+array is strictly smaller than that length. The expression is also checked to
+be positive.
Pattern matching exhaustiveness
*******************************
+Leon verifies that pattern matching is exhaustive. The regular Scala compiler
+only considers the types of expression involved in pattern matching, but Leon
+will consider information such as precondition to formally prove the
+exhaustiveness of pattern matching.
+As an example, the following code should issue a warning with Scala:
+
+.. code-block:: scala
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def getHead(l: List): Int = {
+ require(!l.isInstanceOf[Nil])
+ l match {
+ case Cons(x, _) => x
+ }
+ }
+
+But Leon will actually prove that the pattern matching is actually exhaustive,
+relying on the given precondition.
Proving mathematical theorems with Leon
---------------------------------------
--
GitLab