generic
type Universe is (<>); -- any integer or enumeration type
package Sets_Generic is
------------------------------------------------------------------
--|
--| Specification for sets over discrete universes
--|
--| Author: Michael B. Feldman, The George Washington University
--| Last Modified: October 1995
--|
------------------------------------------------------------------
type Set is private;
Phi: constant Set; -- empty set
-- constructors
function "+" (S: Set; E: Universe) return Set;
function "-" (S: Set; E: Universe) return Set;
-- Pre: S and E are defined
-- Post: returns S with E inserted or deleted respectively;
-- "+" has no effect if IsIn(S,E); "-" has none if NOT IsIn(S,E)
function Singleton(E: Universe) return Set;
function "+" (E1, E2: Universe) return Set;
-- Pre: E, E1, and E2 are defined
-- Post: returns a set made from one or two elements
function "+" (S, T : Set) return Set;
function "*" (S, T : Set) return Set;
function "-" (S, T : Set) return Set;
-- Pre: S and T are defined
-- Post: returns the union, intersection, and difference of
-- S and T, respectively
function "-" (S : Set) return Set;
-- Pre: S is defined
-- Post: returns the complement of S
-- selectors
function IsIn (S : Set; E : Universe) return Boolean;
-- Pre: S and E are defined
-- Post: returns True if and only if E is a member of S
function IsEmpty (S : Set) return Boolean;
-- Pre: S is defined
-- Post: returns True if and only if S is empty
function SizeOf (S : Set) return Natural;
-- Pre: S is defined
-- Post: returns the number of members in S
function "<=" (S, T : Set) return Boolean;
function "<" (S, T : Set) return Boolean;
-- Pre: S and T are defined
-- Post: returns True if and only if S is
-- an improper or proper subset of T, respectively
private
type SetArray is array (Universe) of Boolean;
type Set is record
Store: SetArray := (others => False);
end record;
Phi: constant Set := (Store => (others => False));
end Sets_Generic;