diff --git a/doc/tutorial.rst b/doc/tutorial.rst index 664340104a5d8411149d5531cc3ba2a1ec891c86..55f93f1f59852381ba86aedbba01c9a3a8ba63f2 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: