diff --git a/source/library/vssl-integers-big_decimal.adb b/source/library/vssl-integers-big_decimal.adb index 4ad261b..c52b55d 100644 --- a/source/library/vssl-integers-big_decimal.adb +++ b/source/library/vssl-integers-big_decimal.adb @@ -38,11 +38,14 @@ package body VSSL.Integers.Big_Decimal is renames Digit_Arrays."<"; procedure Set ( - X : in out Big_Decimal_Natural; + X : out Big_Decimal_Natural; Y : in Big_Decimal_Natural) renames Digit_Arrays.Set; - procedure Set (X : in out Big_Decimal_Natural; Y : Natural) is + procedure Set ( + X : out Big_Decimal_Natural; + Y : in Natural) + is T : Natural := Y; begin for I in X'Range loop diff --git a/source/library/vssl-integers-big_decimal.ads b/source/library/vssl-integers-big_decimal.ads index d968734..b076cd3 100644 --- a/source/library/vssl-integers-big_decimal.ads +++ b/source/library/vssl-integers-big_decimal.ads @@ -1,3 +1,5 @@ +pragma SPARK_Mode; + with VSSL.Integers.Decimal_Chunks; with VSSL.Integers.Generic_Digit_Arrays; @@ -27,11 +29,11 @@ package VSSL.Integers.Big_Decimal is function ">=" (X, Y : Big_Decimal_Natural) return Boolean is (not (X < Y)); procedure Set ( - X : in out Big_Decimal_Natural; + X : out Big_Decimal_Natural; Y : in Big_Decimal_Natural); procedure Set ( - X : in out Big_Decimal_Natural; - Y : Natural); + X : out Big_Decimal_Natural; + Y : in Natural); --function "+" (X, Y : Big_Decimal_Natural) return Big_Decimal_Natural; --function "*" (X, Y : Big_Decimal_Natural) return Big_Decimal_Natural; diff --git a/source/library/vssl-integers-generic_digit_arrays.adb b/source/library/vssl-integers-generic_digit_arrays.adb index 7d62a62..99d7352 100644 --- a/source/library/vssl-integers-generic_digit_arrays.adb +++ b/source/library/vssl-integers-generic_digit_arrays.adb @@ -20,18 +20,11 @@ package body VSSL.Integers.Generic_Digit_Arrays is return Index'Base'First; end Last_Nonzero; - function Is_Fit (X, Y : Digit_Array) return Boolean is - begin - return - (Y'First <= X'First - or else Is_Zero (X (X'First .. Index'Min (Index'Pred (Y'First), X'Last)))) - and then - (Y'Last >= X'Last - or else Is_Zero (X (Index'Max (Index'Succ (Y'Last), X'First) .. X'Last))); - end Is_Fit; - function "=" (X, Y : Digit_Array) return Boolean is - pragma Assert (X'First in Index); + pragma Assume (X'First in Index); + pragma Assume (Y'First in Index); + pragma Assume (X'Last in Index); + pragma Assume (Y'Last in Index); -- These assumptions are made for Gnatprove F : Index := Index'Max (X'First, Y'First); L : Index := Index'Min (X'Last, Y'Last); begin @@ -52,6 +45,10 @@ package body VSSL.Integers.Generic_Digit_Arrays is end "="; function "<" (X, Y : Digit_Array) return Boolean is + pragma Assume (X'First in Index); + pragma Assume (Y'First in Index); + pragma Assume (X'Last in Index); + pragma Assume (Y'Last in Index); -- These assumptions are made for Gnatprove XD, YD : Digit_Type; begin for I in reverse Index'Min (X'First, Y'First) .. Index'Max (X'Last, Y'Last) loop @@ -67,21 +64,23 @@ package body VSSL.Integers.Generic_Digit_Arrays is end "<"; -- TODO: optimize procedure Set ( - X : in out Digit_Array; + X : out Digit_Array; Y : in Digit_Array) is - F : Index := Index'Max (X'First, Y'First); - L : Index := Index'Min (X'Last, Y'Last); begin - if not Is_Fit (Y, X) then + if not Is_Fit (Y, X'First, X'Last) then raise Constraint_Error with "Value does not fit in target"; end if; - if F > X'First then - X (X'First .. Index'Pred (F)) := (others => 0); - end if; - X (F .. L) := Y (F .. L); - if L < X'Last then - X (Index'Succ (L) .. X'Last) := (others => 0); + if X'Last < Y'First or else X'First > Y'Last or else X'Length = 0 then + X := (others => 0); + pragma Assert (Left_Equal (X, Y)); + else + for J in X'Range loop + X (J) := (if J in Y'Range then Y (J) else 0); + pragma Loop_Invariant (for all K in X'First .. J => X (K) = (if K in Y'Range then Y (K) else 0)); + pragma Loop_Invariant (Left_Equal (X (X'First .. J), Y)); + end loop; + pragma Assert (Left_Equal (X, Y)); end if; end Set; diff --git a/source/library/vssl-integers-generic_digit_arrays.ads b/source/library/vssl-integers-generic_digit_arrays.ads index 0052287..5fcfc80 100644 --- a/source/library/vssl-integers-generic_digit_arrays.ads +++ b/source/library/vssl-integers-generic_digit_arrays.ads @@ -20,14 +20,25 @@ package VSSL.Integers.Generic_Digit_Arrays is function Last_Nonzero (X : Digit_Array) return Index'Base; -- Returns index of last (most significant) nonzero element or Index'Base'First if all zero - function Is_Fit (X, Y : Digit_Array) return Boolean; - -- Can array X be copied to Y without loss - function Is_Zero (X : Digit_Array) return Boolean is (for all I in X'Range => X (I) = 0); -- Is a digit array represents 0 - function "=" (X, Y : Digit_Array) return Boolean; + function Is_Fit (X : Digit_Array; First, Last : Index'Base) return Boolean + is ((First <= X'First or else Is_Zero (X (X'First .. Index'Min (Index'Pred (First), X'Last)))) + and then + (Last >= X'Last or else Is_Zero (X (Index'Max (Index'Succ (Last), X'First) .. X'Last)))); + -- Can array X be copied to an array with bounds (First .. Last) without loss + + function Is_Fit (X, Y : Digit_Array) return Boolean + is (Is_Fit (X, Y'First, Y'Last)); + -- Can array X be copied to Y without loss + + function Left_Equal (X, Y : Digit_Array) return Boolean + is (for all J in X'Range => X (J) = Element (Y, J)); + + function "=" (X, Y : Digit_Array) return Boolean + with Post => "="'Result = (Left_Equal (X, Y) and Left_Equal (Y, X)); -- Are two digit arrays represent one number function "<" (X, Y : Digit_Array) return Boolean; @@ -40,7 +51,10 @@ package VSSL.Integers.Generic_Digit_Arrays is function ">=" (X, Y : Digit_Array) return Boolean is (not (X < Y)); procedure Set ( - X : in out Digit_Array; - Y : in Digit_Array); + X : out Digit_Array; + Y : in Digit_Array) + with + Pre => Is_Fit (Y, X'First, X'Last), + Post => Left_Equal (X, Y) and Left_Equal (Y, X); end VSSL.Integers.Generic_Digit_Arrays;