From d1c2722c960a8571152dca2a1cae467873cdaef2 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Mon, 27 Apr 2015 11:21:53 -0700
Subject: [PATCH] doc: small fixes in tutorial
---
doc/tutorial.rst | 13 ++++++++-----
1 file changed, 8 insertions(+), 5 deletions(-)
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index 664340104..55f93f1f5 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -296,10 +296,12 @@ specification, such as, for, example:
.. code-block:: scala
- def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
- if (x < y) x
- else y
- }
+ def sort2(x : BigInt, y : BigInt): (BigInt, BigInt) = {
+ if (x < y)
+ (x, y)
+ else
+ (y, x)
+ }
Depending on the particular run, Leon may also produce a solution such as
@@ -349,7 +351,8 @@ In contrast, if we define the corresponding specification for three integers
.. code-block:: scala
def sort3spec(x: BigInt, y: BigInt, z: BigInt, res: (BigInt, BigInt, BigInt)): Boolean = {
- Set(x,y,z) == Set(res._1, res._2, res._3) && res._1 <= res._2 && res._2 <= res._3
+ Set(x,y,z) == Set(res._1, res._2, res._3) &&
+ res._1 <= res._2 && res._2 <= res._3
}
Then uniqueness of the solution is the following conjecture:
--
GitLab