Skip to content
Snippets Groups Projects
Commit d1c2722c authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

doc: small fixes in tutorial

parent f413a659
No related branches found
No related tags found
No related merge requests found
...@@ -296,10 +296,12 @@ specification, such as, for, example: ...@@ -296,10 +296,12 @@ specification, such as, for, example:
.. code-block:: scala .. code-block:: scala
def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) => def sort2(x : BigInt, y : BigInt): (BigInt, BigInt) = {
if (x < y) x if (x < y)
else y (x, y)
} else
(y, x)
}
Depending on the particular run, Leon may also produce a solution such as 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 ...@@ -349,7 +351,8 @@ In contrast, if we define the corresponding specification for three integers
.. code-block:: scala .. code-block:: scala
def sort3spec(x: BigInt, y: BigInt, z: BigInt, res: (BigInt, BigInt, BigInt)): Boolean = { 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: Then uniqueness of the solution is the following conjecture:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment