23 lines
485 B
Plaintext
23 lines
485 B
Plaintext
|
(* BE : Session 1 2020 *)
|
||
|
|
(* Implémentation de la fonction carre d'un entier naturel par un algorithme inspiré des identités remarquables *)
|
||
|
|
|
||
|
|
module Carre
|
||
|
|
|
||
|
|
use int.Int
|
||
|
|
use ref.Refint
|
||
|
|
|
||
|
|
let carre (n: int) : int
|
||
|
|
requires { 0 <= n }
|
||
|
|
ensures { !r = n*n }
|
||
|
|
=
|
||
|
|
let x = ref n in
|
||
|
|
let r = ref 0 in
|
||
|
|
while (!x <> 0) do
|
||
|
|
invariant { !r + (!x)*(!x) = n*n && 0 <= !x }
|
||
|
|
variant { !x }
|
||
|
|
r := (!r) + 2 * (!x) - 1;
|
||
|
|
x := (!x) - 1
|
||
|
|
done;
|
||
|
|
!r
|
||
|
|
|
||
|
|
end
|