128 lines
3.9 KiB
Ada
128 lines
3.9 KiB
Ada
|
with Ada.Text_IO; use Ada.Text_IO;
|
||
|
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
|
||
|
|
||
|
procedure Specifier_Et_Tester is
|
||
|
|
||
|
-- Calculer le plus grand commun diviseur de deux entiers strictement
|
||
|
-- positifs.
|
||
|
-- Paramètres :
|
||
|
-- A : in Entier
|
||
|
-- B : in Entier
|
||
|
-- Retour : Entier -- le pgcd de A et B
|
||
|
-- Nécessite :
|
||
|
-- A > 0
|
||
|
-- B > 0
|
||
|
-- Assure :
|
||
|
-- Pgcd'Result >= 1
|
||
|
-- A mod Pgcd'Résultat = 0 -- le pgcd divise A
|
||
|
-- B mod Pgcd'Résultat = 0 -- le pgcd divise B
|
||
|
-- -- c'est le plus grand des entiers qui divisent A et B
|
||
|
-- // mais on ne sait pas l'exprimer simplement
|
||
|
-- Exemples : voir Tester_Pgcd
|
||
|
-- Efficacité : faible car on utilise une version naïve de l'algorithme
|
||
|
-- d'Euclide.
|
||
|
function Pgcd (A, B : in Integer) return Integer with
|
||
|
Pre => A > 0 and B > 0,
|
||
|
Post => Pgcd'Result >= 1
|
||
|
and A mod Pgcd'Result = 0 -- Le Pgcd divise A
|
||
|
and B mod Pgcd'Result = 0 -- Le Pgcd divise B
|
||
|
is
|
||
|
L_A, L_B: Integer; -- variables correspondant à A et B
|
||
|
-- A et B étant en in, on ne peut pas les modifier dans la
|
||
|
-- fonction. Or pour appliquer l'algortihme d'Euclide, il faut
|
||
|
-- retrancher le plus petit au plus grand jusqu'à avoir deux
|
||
|
-- nombres égaux. Nous passons donc par des variables locales et
|
||
|
-- utilisons le nom des paramètres formels préfixés par 'L_'.
|
||
|
begin
|
||
|
L_A := A;
|
||
|
L_B := B;
|
||
|
while L_A /= L_B loop
|
||
|
-- soustraire au plus grand le plus petit
|
||
|
if L_A > L_B then
|
||
|
L_A := L_A - L_B;
|
||
|
else
|
||
|
L_B := L_B - L_A;
|
||
|
end if;
|
||
|
end loop;
|
||
|
pragma Assert (L_A = L_B); -- la condition de sortie de boucle.
|
||
|
return L_A;
|
||
|
end Pgcd;
|
||
|
|
||
|
|
||
|
-- Exemple d'utilisation du Pgcd.
|
||
|
-- Est-ce que le corps de cette procédure est correct ? Pourquoi ?
|
||
|
-- Que donne son exécution ?
|
||
|
procedure Utiliser_Pgcd is
|
||
|
Resultat: Integer;
|
||
|
begin
|
||
|
Resultat := Pgcd (0, 10);
|
||
|
Put ("Pgcd (0, 10) = ");
|
||
|
Put (Resultat, 1);
|
||
|
New_Line;
|
||
|
end Utiliser_Pgcd;
|
||
|
|
||
|
|
||
|
-- Permuter deux entiers.
|
||
|
-- Paramètres :
|
||
|
-- A, B : in out Entier -- les deux entiers à permuter
|
||
|
-- Nécessite : Néant
|
||
|
-- Assure :
|
||
|
-- A = B'Avant et B = A'Avant -- les valeurs de A et B sont bien permutées
|
||
|
procedure Permuter (A, B: in out Integer) with
|
||
|
Post => A = B'Old and B = A'Old
|
||
|
is
|
||
|
Copie_A : Integer;
|
||
|
begin
|
||
|
Copie_A := A;
|
||
|
A := B;
|
||
|
B := Copie_A;
|
||
|
end Permuter;
|
||
|
|
||
|
|
||
|
-- Procédure de test de Pgcd.
|
||
|
-- -- Parce que c'est une procédure de test, elle n'a pas de paramètre,
|
||
|
-- -- pas de type de retour, pas de précondition, pas de postcondition.
|
||
|
procedure Tester_Pgcd is
|
||
|
begin
|
||
|
pragma Assert (4 = Pgcd (4, 4)); -- A = B
|
||
|
pragma Assert (2 = Pgcd (10, 16)); -- A < B
|
||
|
pragma Assert (1 = Pgcd (21, 10)); -- A > B
|
||
|
pragma Assert (3 = Pgcd (105, 147)); -- un autre
|
||
|
end Tester_Pgcd;
|
||
|
|
||
|
|
||
|
-- Procédure de test pour mettre en évidence la faible efficacité de Pgcd.
|
||
|
procedure Tester_Performance_Pgcd is
|
||
|
begin
|
||
|
pragma Assert (1 = Pgcd (1, 10 ** 9)); -- lent !
|
||
|
end Tester_Performance_Pgcd;
|
||
|
|
||
|
|
||
|
-- Procédure de test de Permuter.
|
||
|
procedure Tester_Permuter is
|
||
|
N1, N2: Integer;
|
||
|
begin
|
||
|
-- initialiser les données du test
|
||
|
N1 := 5;
|
||
|
N2 := 18;
|
||
|
|
||
|
-- lancer la procédure à tester
|
||
|
Permuter (N1, N2);
|
||
|
|
||
|
-- contrôler que la procédure a eu l'effet escompté
|
||
|
pragma Assert (18 = N1);
|
||
|
pragma Assert (5 = N2);
|
||
|
end Tester_Permuter;
|
||
|
|
||
|
|
||
|
begin
|
||
|
Utiliser_Pgcd;
|
||
|
|
||
|
-- lancer les programmes de test.
|
||
|
Tester_Pgcd;
|
||
|
Tester_Performance_Pgcd;
|
||
|
Tester_Permuter;
|
||
|
Put_Line ("Fini.");
|
||
|
|
||
|
end Specifier_Et_Tester;
|