Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 63ad8e88 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

trywhy3: better example isqrt

parent c348848e
......@@ -5,6 +5,9 @@ module M
function sqr (x:int) : int = x * x
lemma sqr_sum :
forall x y : int. sqr(x+y) = sqr x + 2*x*y + sqr y
let isqrt (x:int) : int
requires { x >= 0 }
ensures { result >= 0 }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment