(* Exact Integer square root *) use int.Int function sqr(n:int) : int = n * n (* lemma sqr_increasing: forall x y:int. 0 <= x < y -> sqr x < sqr y lemma sqr_neg: forall x:int. sqr (-x) = sqr x *) exception NotSquare let isqrt (x:int) : int ensures { result >= 0 /\ sqr result = x } raises { NotSquare -> forall n:int. sqr n <> x } = if x < 0 then raise NotSquare; let ref res = 0 in let ref sum = 1 in while sum <= x do invariant { res >= 0 } invariant { x >= sqr res } invariant { sum = sqr (res+1) } res <- res + 1; sum <- sum + 2 * res + 1 done; if res * res <> x then begin assert { sqr res < x }; assert { sqr (res+1) > x }; assert { forall n:int. 0 <= n <= res -> sqr n < x }; assert { forall n:int. n > res -> sqr n > x }; raise NotSquare end; res (* Local Variables: compile-command: "why3 ide isqrt_exc.mlw" End: *)