diff options
Diffstat (limited to 'gcc/ada/libgnat/s-expmod.adb')
| -rw-r--r-- | gcc/ada/libgnat/s-expmod.adb | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb index 0682589d352..aa6e9b4c361 100644 --- a/gcc/ada/libgnat/s-expmod.adb +++ b/gcc/ada/libgnat/s-expmod.adb @@ -109,9 +109,21 @@ is procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) with Pre => F /= 0, - Post => (Q * F + R) mod F = R mod F; + Post => (Q * F + R) mod F = R mod F, + Subprogram_Variant => (Decreases => Q); - procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is null; + ------------------------- + -- Lemma_Euclidean_Mod -- + ------------------------- + + procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is + begin + if Q > 0 then + Lemma_Euclidean_Mod (Q - 1, F, R); + end if; + end Lemma_Euclidean_Mod; + + -- Local variables Left : constant Big_Natural := (X + Y) mod B; Right : constant Big_Natural := ((X mod B) + (Y mod B)) mod B; @@ -164,6 +176,9 @@ is Lemma_Mod_Mod (A, B); Lemma_Exp_Mod (A, Exp - 1, B); Lemma_Mult_Mod (A, A ** (Exp - 1), B); + pragma Assert + ((A mod B) * (A mod B) ** (Exp - 1) = (A mod B) ** Exp); + pragma Assert (A * A ** (Exp - 1) = A ** Exp); pragma Assert (Left = Right); end; end if; @@ -190,6 +205,7 @@ is pragma Assert (Left = Right); else pragma Assert (Y mod B = 0); + pragma Assert (Y / B * B = Y); pragma Assert ((X * Y) mod B = (X * Y) - (X * Y) / B * B); pragma Assert ((X * Y) mod B = (X * Y) - (X * (Y / B) * B) / B * B); |