Try to prove Integers.Generic_Digit_Arrays.Set
This commit is contained in:
parent
a5525ecc79
commit
41a731c95a
|
@ -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
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in New Issue