From 216ffee12c880aad31aaed5b1ce012b68d6607fb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 20 Apr 2015 16:49:28 +0200
Subject: [PATCH] Fix warning
---
doc/intro.rst | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/doc/intro.rst b/doc/intro.rst
index a3964da4b..d1d4e8b5f 100644
--- a/doc/intro.rst
+++ b/doc/intro.rst
@@ -28,9 +28,14 @@ it would prove that the postcondition always hold, assuming a given precondition
hold. A simple example:
.. code-block:: scala
+
def factorial(n: Int): Int = {
require(n >= 0)
- if(n == 0) 1 else n * factorial(n - 1)
+ if(n == 0) {
+ 1
+ } else {
+ n * factorial(n - 1)
+ }
} ensuring(res => res >= 0)
Leon generates a ``postcondition`` verification condition for the above
@@ -56,10 +61,11 @@ Leon supports verification of a significant part of the Scala language, describe
sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`.
-Automated Repair of Programs
-----------------------------
Program Synthesis
-----------------
+
+Program Repair
+--------------
--
GitLab