39 lines
776 B
Plaintext
Executable file
39 lines
776 B
Plaintext
Executable file
|
|
(* PGCD : Algorithme Euclide *)
|
|
|
|
theory PGCD
|
|
|
|
use int.Int
|
|
|
|
function pgcd(a b : int) : int
|
|
|
|
axiom A1 : forall a: int. (a>0) -> ( pgcd a a ) = a
|
|
axiom A2 : forall a,b: int. (a>0 && b>0) -> ( pgcd a b ) = ( pgcd b a )
|
|
axiom A3 : forall a,b: int. (a>b>0) -> ( pgcd a b ) = (pgcd (a-b) b )
|
|
|
|
end
|
|
|
|
module PGCDEuclide
|
|
|
|
use import int.Int
|
|
use import ref.Refint
|
|
use import PGCD
|
|
|
|
let pgcd_euclide (a b: int) : int
|
|
requires { 0 < a && 0 < b }
|
|
ensures { result = (pgcd a b)}
|
|
=
|
|
let ap = ref a in
|
|
let bp = ref b in
|
|
while (!ap <> !bp) do
|
|
invariant { (pgcd a b ) = ( pgcd !ap !bp ) && !ap > 0 && !bp > 0 }
|
|
variant { !ap + !bp }
|
|
if (!ap <= !bp) then
|
|
bp := !bp - !ap
|
|
else
|
|
ap := !ap - !bp
|
|
done;
|
|
!ap
|
|
|
|
end
|