isqrt.mlw 2.09 KB
 Jean-Christophe Filliatre committed Apr 03, 2011 1 `````` `````` MARCHE Claude committed Jul 09, 2015 2 ``````(** {1 Integer square root} *) `````` Jean-Christophe Filliatre committed Apr 03, 2011 3 `````` `````` MARCHE Claude committed Jul 09, 2015 4 ``````module Square `````` MARCHE Claude committed Nov 03, 2010 5 `````` `````` Jean-Christophe Filliatre committed Dec 30, 2010 6 7 `````` use import int.Int `````` Andrei Paskevich committed Jun 29, 2011 8 `````` function sqr (x:int) : int = x * x `````` MARCHE Claude committed Nov 03, 2010 9 `````` `````` MARCHE Claude committed Mar 07, 2016 10 11 `````` lemma sqr_non_neg: forall x:int. sqr x >= 0 `````` MARCHE Claude committed Jul 09, 2015 12 13 14 `````` lemma sqr_increasing: forall x y:int. 0 <= x <= y -> sqr x <= sqr y `````` MARCHE Claude committed Mar 07, 2016 15 16 17 `````` lemma sqr_sum : forall x y : int. sqr(x+y) = sqr x + 2*x*y + sqr y `````` MARCHE Claude committed Jul 09, 2015 18 19 20 21 22 23 24 25 26 27 28 29 `````` predicate isqrt_spec (x res:int) = res >= 0 /\ sqr res <= x < sqr (res + 1) end (** {2 Simple algorithm} *) module Simple use import int.Int use import ref.Ref use import Square `````` Andrei Paskevich committed Oct 13, 2012 30 31 `````` let isqrt (x:int) : int requires { x >= 0 } `````` MARCHE Claude committed Jul 09, 2015 32 `````` ensures { isqrt_spec x result } `````` Andrei Paskevich committed Oct 13, 2012 33 `````` = let count = ref 0 in `````` Jean-Christophe Filliatre committed Jan 24, 2011 34 35 `````` let sum = ref 1 in while !sum <= x do `````` MARCHE Claude committed Nov 16, 2016 36 37 38 `````` invariant { !count >= 0 } invariant { x >= sqr !count } invariant { !sum = sqr (!count+1) } `````` Jean-Christophe Filliatre committed May 20, 2011 39 `````` variant { x - !count } `````` Jean-Christophe Filliatre committed Jan 24, 2011 40 41 42 43 44 `````` count := !count + 1; sum := !sum + 2 * !count + 1 done; !count `````` MARCHE Claude committed Jul 09, 2015 45 46 47 `````` let main () ensures { result = 4 } = isqrt 17 `````` MARCHE Claude committed Nov 03, 2010 48 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 49 ``````end `````` MARCHE Claude committed Nov 03, 2010 50 `````` `````` MARCHE Claude committed Jul 09, 2015 51 ``````(** {2 Another algorithm, in the style of Newton-Raphson} *) `````` 52 53 54 55 56 `````` module NewtonMethod use import int.Int use import int.ComputerDivision `````` Andrei Paskevich committed Oct 13, 2012 57 `````` use import ref.Ref `````` MARCHE Claude committed Jul 09, 2015 58 `````` use import Square `````` 59 `````` `````` MARCHE Claude committed Jul 09, 2015 60 61 62 63 `````` let sqrt (x : int) : int requires { x >= 0 } ensures { isqrt_spec x result } = if x = 0 then 0 else `````` 64 65 `````` if x <= 3 then 1 else let y = ref x in `````` MARCHE Claude committed Mar 07, 2016 66 `````` let z = ref (div (1 + x) 2) in `````` 67 68 `````` while !z < !y do variant { !y } `````` MARCHE Claude committed Jul 08, 2015 69 70 71 `````` invariant { !z > 0 } invariant { !y > 0 } invariant { !z = div (div x !y + !y) 2 } `````` MARCHE Claude committed Jul 09, 2015 72 73 `````` invariant { x < sqr (!y + 1) } invariant { x < sqr (!z + 1) } `````` 74 `````` y := !z; `````` MARCHE Claude committed Jul 09, 2015 75 76 `````` z := div (div x !z + !z) 2; (* A few hints to prove preservation of the last invariant *) `````` MARCHE Claude committed Nov 16, 2016 77 78 79 80 81 82 `````` assert { x < sqr (!z + 1) by let a = div x !y in x < a * !y + !y so a + !y <= 2 * !z + 1 so sqr (a + !y + 1) <= sqr (2 * !z + 2) so 4 * (sqr (!z + 1) - x) `````` MARCHE Claude committed Jul 09, 2015 83 84 85 86 87 `````` = sqr (2 * !z + 2) - 4 * x >= sqr (a + !y + 1) - 4 * x > sqr (a + !y + 1) - 4 * (a * !y + !y) = sqr (a + 1 - !y) >= 0 } `````` 88 `````` done; `````` MARCHE Claude committed Nov 16, 2016 89 90 `````` assert { !y * !y <= div x !y * !y by !y <= div x !y }; `````` 91 92 93 `````` !y end``````