return True;
end Elements_Equal_Except;
+ ---------------
+ -- Empty_Map --
+ ---------------
+
+ function Empty_Map return Map is
+ ((others => <>));
+
---------
-- Get --
---------
and Container <= Add'Result
and Keys_Included_Except (Add'Result, Container, New_Key);
+ function Empty_Map return Map with
+ -- Return an empty Map
+
+ Global => null,
+ Post =>
+ Length (Empty_Map'Result) = 0
+ and Is_Empty (Empty_Map'Result);
+
function Remove
(Container : Map;
Key : Key_Type) return Map
function Contains (Container : Set; Item : Element_Type) return Boolean is
(Find (Container.Content, Item) > 0);
+ ---------------
+ -- Empty_Set --
+ ---------------
+
+ function Empty_Set return Set is
+ ((others => <>));
+
---------------------
-- Included_Except --
---------------------
and Container <= Add'Result
and Included_Except (Add'Result, Container, Item);
+ function Empty_Set return Set with
+ -- Return an new empty set
+
+ Global => null,
+ Post => Is_Empty (Empty_Set'Result);
+
function Remove (Container : Set; Item : Element_Type) return Set with
-- Return a new set containing all the elements of Container except E
return False;
end Contains;
+ --------------------
+ -- Empty_Sequence --
+ --------------------
+
+ function Empty_Sequence return Sequence is
+ ((others => <>));
+
------------------
-- Equal_Except --
------------------
-- i.e. it does not contain pointers that could be used to alias mutable
-- data).
+ function Empty_Sequence return Sequence with
+ -- Return an empty Sequence
+
+ Global => null,
+ Post => Length (Empty_Sequence'Result) = 0;
+
---------------------------
-- Iteration Primitives --
---------------------------