Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 0a9d9bb0 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

isqrt

parent 27a09f65
{
logic sqr (x:int) : int = x * x
}
let isqrt (x:int) =
{ x >= 0 }
let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { !count >= 0 and
x >= sqr !count and
!sum = sqr (!count+1) }
variant { x - !sum }
count := !count + 1;
sum := !sum + 2 * !count + 1
done;
!count
{ result >= 0 and sqr result <= x and x < sqr (result + 1) }
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