@@ -29,7 +29,17 @@
-- --
------------------------------------------------------------------------------
-package body System.Vectors.Boolean_Operations 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);
+
+package body System.Vectors.Boolean_Operations
+ with SPARK_Mode
+is
SU : constant := Storage_Unit;
-- Convenient short hand, used throughout
@@ -76,7 +86,26 @@ package body System.Vectors.Boolean_Operations is
-----------
function "not" (Item : Vectors.Vector) return Vectors.Vector is
+
+ procedure Prove_Not (Result : Vectors.Vector)
+ with
+ Ghost,
+ Pre => Valid (Item)
+ and then Result = (Item xor True_Val),
+ Post => Valid (Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Result) (J) = not Model (Item) (J));
+
+ procedure Prove_Not (Result : Vectors.Vector) is
+ begin
+ for J in 1 .. Vector_Boolean_Size loop
+ pragma Assert
+ (Element (Result, J) = 1 - Element (Item, J));
+ end loop;
+ end Prove_Not;
+
begin
+ Prove_Not (Item xor True_Val);
return Item xor True_Val;
end "not";
@@ -90,7 +119,32 @@ package body System.Vectors.Boolean_Operations is
end Nand;
function Nand (Left, Right : Vectors.Vector) return Vectors.Vector is
+
+ procedure Prove_And (Result : Vectors.Vector)
+ with
+ Ghost,
+ Pre => Valid (Left)
+ and then Valid (Right)
+ and then Result = (Left and Right),
+ Post => Valid (Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Result) (J) =
+ (Model (Left) (J) and Model (Right) (J)));
+
+ procedure Prove_And (Result : Vectors.Vector) is
+ begin
+ for J in 1 .. Vector_Boolean_Size loop
+ pragma Assert
+ (Element (Result, J) =
+ (if Element (Left, J) = 1
+ and Element (Right, J) = 1
+ then 1
+ else 0));
+ end loop;
+ end Prove_And;
+
begin
+ Prove_And (Left and Right);
return not (Left and Right);
end Nand;
@@ -104,7 +158,32 @@ package body System.Vectors.Boolean_Operations is
end Nor;
function Nor (Left, Right : Vectors.Vector) return Vectors.Vector is
+
+ procedure Prove_Or (Result : Vectors.Vector)
+ with
+ Ghost,
+ Pre => Valid (Left)
+ and then Valid (Right)
+ and then Result = (Left or Right),
+ Post => Valid (Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Result) (J) =
+ (Model (Left) (J) or Model (Right) (J)));
+
+ procedure Prove_Or (Result : Vectors.Vector) is
+ begin
+ for J in 1 .. Vector_Boolean_Size loop
+ pragma Assert
+ (Element (Result, J) =
+ (if Element (Left, J) = 1
+ or Element (Right, J) = 1
+ then 1
+ else 0));
+ end loop;
+ end Prove_Or;
+
begin
+ Prove_Or (Left or Right);
return not (Left or Right);
end Nor;
@@ -118,7 +197,32 @@ package body System.Vectors.Boolean_Operations is
end Nxor;
function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector is
+
+ procedure Prove_Xor (Result : Vectors.Vector)
+ with
+ Ghost,
+ Pre => Valid (Left)
+ and then Valid (Right)
+ and then Result = (Left xor Right),
+ Post => Valid (Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Result) (J) =
+ (Model (Left) (J) xor Model (Right) (J)));
+
+ procedure Prove_Xor (Result : Vectors.Vector) is
+ begin
+ for J in 1 .. Vector_Boolean_Size loop
+ pragma Assert
+ (Element (Result, J) =
+ (if Element (Left, J) = 1
+ xor Element (Right, J) = 1
+ then 1
+ else 0));
+ end loop;
+ end Prove_Xor;
+
begin
+ Prove_Xor (Left xor Right);
return not (Left xor Right);
end Nxor;
@@ -31,15 +31,77 @@
-- This package contains functions for runtime operations on boolean vectors
-package System.Vectors.Boolean_Operations is
- pragma Pure;
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
+package System.Vectors.Boolean_Operations
+ with Pure, SPARK_Mode
+is
+ pragma Warnings (Off, "aspect ""Pre"" not enforced on inlined subprogram",
+ Reason => "Pre only used in proof");
+ pragma Warnings (Off, "aspect ""Post"" not enforced on inlined subprogram",
+ Reason => "Post only used in proof");
+
+ -- Type Vectors.Vector represents an array of Boolean, each of which
+ -- takes 8 bits of the representation, with the 7 msb set to zero. Express
+ -- in contracts the constraint on valid vectors and the model that they
+ -- represent, and the relationship between input models and output model.
+
+ Vector_Boolean_Size : constant Positive :=
+ System.Word_Size / System.Storage_Unit
+ with Ghost;
+
+ type Vector_Element is mod 2 ** System.Storage_Unit with Ghost;
+
+ type Vector_Boolean_Array is array (1 .. Vector_Boolean_Size) of Boolean
+ with Ghost;
+
+ function Shift_Right (V : Vectors.Vector; N : Natural) return Vectors.Vector
+ with Ghost, Import, Convention => Intrinsic;
+
+ function Element (V : Vectors.Vector; N : Positive) return Vector_Element is
+ (Vector_Element (Shift_Right (V, (N - 1) * System.Storage_Unit)
+ and (2 ** System.Storage_Unit - 1)))
+ with
+ Ghost,
+ Pre => N <= Vector_Boolean_Size;
+ -- Return the Nth element represented by the vector
+
+ function Valid (V : Vectors.Vector) return Boolean is
+ (for all J in 1 .. Vector_Boolean_Size =>
+ Element (V, J) in 0 .. 1)
+ with Ghost;
+ -- A valid vector is one for which all elements are 0 (representing False)
+ -- or 1 (representing True).
+
+ function Model (V : Vectors.Vector) return Vector_Boolean_Array
+ with
+ Ghost,
+ Pre => Valid (V);
+
+ function Model (V : Vectors.Vector) return Vector_Boolean_Array is
+ (for J in 1 .. Vector_Boolean_Size => Element (V, J) = 1);
+ -- The model of a valid vector is the corresponding array of Boolean values
-- Although in general the boolean operations on arrays of booleans are
-- identical to operations on arrays of unsigned words of the same size,
-- for the "not" operator this is not the case as False is typically
-- represented by 0 and true by 1.
- function "not" (Item : Vectors.Vector) return Vectors.Vector;
+ function "not" (Item : Vectors.Vector) return Vectors.Vector
+ with
+ Pre => Valid (Item),
+ Post => Valid ("not"'Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model ("not"'Result) (J) = not Model (Item) (J));
-- The three boolean operations "nand", "nor" and "nxor" are needed
-- for cases where the compiler moves boolean array operations into
@@ -51,13 +113,44 @@ package System.Vectors.Boolean_Operations is
-- (not X) xor (not Y) = X xor Y
-- X xor (not Y) = not (X xor Y) = Nxor (X, Y)
- function Nand (Left, Right : Boolean) return Boolean;
- function Nor (Left, Right : Boolean) return Boolean;
- function Nxor (Left, Right : Boolean) return Boolean;
+ function Nand (Left, Right : Boolean) return Boolean
+ with
+ Post => Nand'Result = not (Left and Right);
+
+ function Nor (Left, Right : Boolean) return Boolean
+ with
+ Post => Nor'Result = not (Left or Right);
+
+ function Nxor (Left, Right : Boolean) return Boolean
+ with
+ Post => Nxor'Result = not (Left xor Right);
+
+ function Nand (Left, Right : Vectors.Vector) return Vectors.Vector
+ with
+ Pre => Valid (Left)
+ and then Valid (Right),
+ Post => Valid (Nand'Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Nand'Result) (J) =
+ Nand (Model (Left) (J), Model (Right) (J)));
+
+ function Nor (Left, Right : Vectors.Vector) return Vectors.Vector
+ with
+ Pre => Valid (Left)
+ and then Valid (Right),
+ Post => Valid (Nor'Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Nor'Result) (J) =
+ Nor (Model (Left) (J), Model (Right) (J)));
- function Nand (Left, Right : Vectors.Vector) return Vectors.Vector;
- function Nor (Left, Right : Vectors.Vector) return Vectors.Vector;
- function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector;
+ function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector
+ with
+ Pre => Valid (Left)
+ and then Valid (Right),
+ Post => Valid (Nxor'Result)
+ and then (for all J in 1 .. Vector_Boolean_Size =>
+ Model (Nxor'Result) (J) =
+ Nxor (Model (Left) (J), Model (Right) (J)));
pragma Inline_Always ("not");
pragma Inline_Always (Nand);