@@ -34,8 +34,9 @@
with System.Width_U;
with System.Unsigned_Types;
-package System.Wid_LLLU is
-
+package System.Wid_LLLU
+ with SPARK_Mode
+is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
function Width_Long_Long_Long_Unsigned is
@@ -34,8 +34,9 @@
with System.Width_U;
with System.Unsigned_Types;
-package System.Wid_LLU is
-
+package System.Wid_LLU
+ with SPARK_Mode
+is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
function Width_Long_Long_Unsigned is new Width_U (Long_Long_Unsigned);
@@ -29,10 +29,87 @@
-- --
------------------------------------------------------------------------------
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
function System.Width_U (Lo, Hi : Uns) return Natural is
+
+ -- Ghost code, loop invariants and assertions in this unit are meant for
+ -- analysis only, not for run-time checking, as it would be too costly
+ -- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+ pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
W : Natural;
T : Uns;
+ package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
+
+ function Big (Arg : Uns) return Big_Integer is
+ (Unsigned_Conversion.To_Big_Integer (Arg))
+ with Ghost;
+
+ -- Maximum value of exponent for 10 that fits in Uns'Base
+ function Max_Log10 return Natural is
+ (case Uns'Base'Size is
+ when 8 => 2,
+ when 16 => 4,
+ when 32 => 9,
+ when 64 => 19,
+ when 128 => 38,
+ when others => raise Program_Error)
+ with Ghost;
+
+ Max_W : constant Natural := Max_Log10 with Ghost;
+ Big_10 : constant Big_Integer := Big (10) with Ghost;
+
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
+ with
+ Ghost,
+ Pre => A <= B,
+ Post => A * C <= B * C;
+
+ procedure Lemma_Div_Commutation (X, Y : Uns)
+ with
+ Ghost,
+ Pre => Y /= 0,
+ Post => Big (X) / Big (Y) = Big (X / Y);
+
+ procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive)
+ with
+ Ghost,
+ Post => X / Y / Z = X / (Y * Z);
+
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is
+ begin
+ null;
+ end Lemma_Lower_Mult;
+
+ procedure Lemma_Div_Commutation (X, Y : Uns) is
+ begin
+ null;
+ end Lemma_Div_Commutation;
+
+ procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
+ XY : constant Big_Natural := X / Y;
+ YZ : constant Big_Natural := Y * Z;
+ XYZ : constant Big_Natural := X / Y / Z;
+ R : constant Big_Natural := (XY rem Z) * Y + (X rem Y);
+ begin
+ pragma Assert (X = XY * Y + (X rem Y));
+ pragma Assert (XY = XY / Z * Z + (XY rem Z));
+ pragma Assert (X = XYZ * YZ + R);
+ pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y);
+ pragma Assert (R <= YZ - 1);
+ pragma Assert (X / YZ = (XYZ * YZ + R) / YZ);
+ pragma Assert (X / YZ = XYZ + R / YZ);
+ end Lemma_Div_Twice;
+
+ Pow : Big_Integer := 1 with Ghost;
+ T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost;
+
begin
if Lo > Hi then
return 0;
@@ -50,10 +127,40 @@ begin
-- Increase value if more digits required
while T >= 10 loop
+ Lemma_Div_Commutation (T, 10);
+ Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10);
+
T := T / 10;
W := W + 1;
+ Pow := Pow * 10;
+
+ pragma Loop_Variant (Decreases => T);
+ pragma Loop_Invariant (W in 3 .. Max_W + 3);
+ pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
+ pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
end loop;
+ declare
+ F : constant Big_Integer := Big_10 ** (W - 2) with Ghost;
+ Q : constant Big_Integer := Big (T_Init) / F with Ghost;
+ R : constant Big_Integer := Big (T_Init) rem F with Ghost;
+ begin
+ pragma Assert (Q < Big_10);
+ pragma Assert (Big (T_Init) = Q * F + R);
+ Lemma_Lower_Mult (Q, Big (9), F);
+ pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
+ pragma Assert (Big (T_Init) < Big_10 * F);
+ pragma Assert (Big_10 * F = Big_10 ** (W - 1));
+ end;
+
+ -- This is an expression of the functional postcondition for Width_U,
+ -- which cannot be expressed readily as a postcondition as this would
+ -- require making the instantiation Unsigned_Conversion and function
+ -- Big available from the spec.
+
+ pragma Assert (Big (Lo) < Big_10 ** (W - 1));
+ pragma Assert (Big (Hi) < Big_10 ** (W - 1));
+
return W;
end if;
@@ -34,8 +34,9 @@
with System.Width_U;
with System.Unsigned_Types;
-package System.Wid_Uns is
-
+package System.Wid_Uns
+ with SPARK_Mode
+is
subtype Unsigned is Unsigned_Types.Unsigned;
function Width_Unsigned is new Width_U (Unsigned);