25 lines
501 B
Plaintext
Executable file
25 lines
501 B
Plaintext
Executable file
(* BE : Session 1 2019 *)
|
|
(* Implémentation de la fonction somme des premiers entiers par un algorithme ascendant *)
|
|
|
|
module Somme
|
|
|
|
use int.Int
|
|
use int.ComputerDivision
|
|
use ref.Refint
|
|
|
|
let somme (n: int) : int
|
|
requires { n >= 0 }
|
|
ensures { 2 * result = n * (n+1) }
|
|
=
|
|
let i = ref 0 in
|
|
let r = ref 0 in
|
|
while (!i < n) do
|
|
invariant { !r * 2 = !i * ( !i + 1 ) && n >= !i}
|
|
variant { n - !i }
|
|
i := (!i) + 1;
|
|
r := (!r) + (!i)
|
|
done;
|
|
!r
|
|
|
|
end
|