A.18.7 Sets

Ramification: If the actual function for "=" is not symmetric and consistent, the result returned by the "=" for Set objects cannot be predicted. The implementation is not required to protect against "=" raising an exception, or returning random results, or any other “bad” behavior. And it can call "=" in whatever manner makes sense. But note that only the result of "=" for Set objects is unspecified; other subprograms are not allowed to break if "=" is bad (they aren't expected to use "="). 

Discussion: {AI12-0112-1} Note that Replace_Element tampers with cursors because it might delete and reinsert the element if it moves in the set. That could change the order of iteration, which is what this check is designed to prevent. Replace also tampers with cursors, as it is defined in terms of Replace_Element.

{AI12-0112-1} These inclusions mean that there are no operations that would tamper with elements that do not tamper with cursors. As such, we do not define tampering with elements at all for set containers. Earlier versions of Ada did so just so the description of subprograms are the same between containers, but since we've changed those to pre- and postconditions which are necessarily specific to each container, there no longer seems to be any reason to define tampering with elements for sets. 

Ramification: We don't need to explicitly mention assignment_statement, because that finalizes the target object as part of the operation, and finalization of an object is already defined as tampering with cursors.

To be honest: {AI12-0434-1} “The primitive "=" operator” is the one with two parameters of type Cursor which returns Boolean. We're not talking about some other (hidden) primitive function named "=". 

Reason: A cursor will probably be implemented in terms of one or more access values, and the effects of streaming access values is unspecified. Rather than letting the user stream junk by accident, we mandate that streaming of cursors raise Program_Error by default. The attributes can always be specified if there is a need to support streaming. 

Ramification: Streaming more elements than the container length is wrong. For implementation implications of this rule, see the Implementation Note in A.18.2.

To be honest: {AI05-0005-1} {AI05-0212-1} This function might not detect cursors that designate deleted elements; such cursors are invalid (see below) and the result of calling Has_Element with an invalid cursor is unspecified (but not erroneous). 

Ramification: {AI12-0112-1} If Position is No_Element, Has_Element returns False. 

Implementation Note: This wording describes the canonical semantics. However, the order and number of calls on the formal equality function is unspecified for all of the operations that use it in this package, so an implementation can call it as many or as few times as it needs to get the correct answer. Specifically, there is no requirement to call the formal equality additional times once the answer has been determined. 

Implementation Note: {AI12-0112-1} Various contracts elsewhere in this specification require that this function be implemented with synchronized data. Moreover, it is possible for tampering to be prohibited by multiple operations (sequentially or in parallel). Therefore, tampering needs to be implemented with an atomic or protected counter. The counter is initialized to zero, and is incremented when tampering is prohibited, and decremented when leaving an area that prohibited tampering. Function Tampering_With_Cursors_Prohibited returns True if the counter is nonzero. (Note that any case where the result is not well-defined for one task is incorrect use of shared variables and would be erroneous by the rules of 9.10, so no special protection is needed to read the counter.) 

Implementation Note: The final assignment may require that the node of the element be moved in the Set's data structures. That could mean that implementing this operation exactly as worded above could require the overhead of searching twice. Implementations are encouraged to avoid this extra overhead when possible, by prechecking if the old element is equivalent to the new one, by inserting a placeholder node while checking for an equivalent element, and similar optimizations.

The cursor still designates the same element after this operation; only the value of that element has changed. Cursors cannot include information about the relative position of an element in a Set (as they must survive insertions and deletions of other elements), so this should not pose an implementation hardship. 

Reason: It is expected that Constant_Reference_Type will be a controlled type, for which finalization will have some action to terminate the tampering check for the associated container. If the object is created by default, however, there is no associated container. Since this is useless, and supporting this case would take extra work, we define it to raise an exception. 

Discussion: {AI05-0005-1} This routine exists for compatibility with the bounded set containers. For an unbounded set, Assign(A, B) and A := B behave identically. For a bounded set, := will raise an exception if the container capacities are different, while Assign will not raise an exception if there is enough room in the target. 

Discussion: This is equivalent to: 

but doesn't require the hassle of out parameters. 

Ramification: The check on Position checks that the cursor does not belong to some other set. This check implies that a reference to the set is included in the cursor value. This wording is not meant to require detection of dangling cursors; such cursors are defined to be invalid, which means that execution is erroneous, and any result is allowed (including not raising an exception). 

Implementation Note: If the objects are the same, the result is the same as the original object. The implementation needs to take care so that aliasing effects do not make the result trash; Union (S, S); must work. 

Implementation Note: If the objects are the same, the result is the same as the original object. The implementation needs to take care so that aliasing effects do not make the result trash; Intersection (S, S); must work. 

Discussion: This operation is commutative. If Overlap returns False, the two sets are disjoint. 

Discussion: This operation is not commutative, so we use parameter names that make it clear in named notation which set is which. 

Implementation Note: The “tamper with cursors” check takes place when the operations that insert or delete elements, and so on are called.

See Iterate for vectors (A.18.2) for a suggested implementation of the check. 

Reason: The key check ensures that the invariants of the set are preserved by the modification. The “tampers with the elements” check prevents data loss (if Element_Type is by-copy) or erroneous execution (if element type is unconstrained and indefinite). 

Ramification: This means that the elements cannot be directly allocated from the heap; it must be possible to change the discriminants of the element in place. 

Discussion: The Generic_Keys package is not included in the Stable package. The functions Union, Intersection, Difference, and Symmetric_Difference are included in the Stable package.

Ramification: The names Set and Cursor mean the types declared in the nested package in these subprogram specifications.

Reason: The omitted routines are those that tamper with cursors (or test that state). The model is that it is impossible to tamper with cursors of a stable view since no such operations are included. Thus tampering checks are not needed for a stable view, and we omit the operations associated with those checks. 

Proof: {AI12-0438-1} Initialization is required as the type is indefinite, see 3.3.1.

Ramification: {AI05-0160-1} This can happen directly via calls to Clear, Exclude, Delete, and Update_Element_Preserving_Key, and indirectly via calls to procedures Intersection, Difference, and Symmetric_Difference. 

Discussion: The list above is intended to be exhaustive. In other cases, a cursor value continues to designate its original element. For instance, cursor values survive the insertion and deletion of other elements.

While it is possible to check for these cases, in many cases the overhead necessary to make the check is substantial in time or space. Implementations are encouraged to check for as many of these cases as possible and raise Program_Error if detected. 

Reason: Each object of Reference_Type and Constant_Reference_Type probably contains some reference to the originating container. If that container is prematurely finalized (which is only possible via Unchecked_Deallocation, as accessibility checks prevent passing a container to Reference that will not live as long as the result), the finalization of the object of Reference_Type will try to access a nonexistent object. This is a normal case of a dangling pointer created by Unchecked_Deallocation; we have to explicitly mention it here as the pointer in question is not visible in the specification of the type. (This is the same reason we have to say this for invalid cursors.) 

Implementation Note: {AI05-0298-1} An assignment of a Set is a “deep” copy; that is the elements are copied as well as the data structures. We say “effect of” in order to allow the implementation to avoid copying elements immediately if it wishes. For instance, an implementation that avoided copying until one of the containers is modified would be allowed. (Note that this implementation would require care, see A.18.2 for more.)

Implementation Advice: Move for sets should not copy elements, and should minimize copying of internal data structures.

Implementation Note: Usually that can be accomplished simply by moving the pointer(s) to the internal data structures from the Source container to the Target container. 

Implementation Advice: If an exception is propagated from a set operation, no storage should be lost, nor any elements removed from a set unless specified by the operation.

Reason: This is important so that programs can recover from errors. But we don't want to require heroic efforts, so we just require documentation of cases where this can't be accomplished.

{AI95-00302-03} This description of sets is new; the extensions are documented with the specific packages. 

{AI05-0212-1} Added reference support to make set containers more convenient to use. 

{AI05-0001-1} Added procedure Assign; the extension and incompatibility is documented with the specific packages.

{AI05-0001-1} Generalized the definition of Move. Specified which elements are read/written by stream attributes.

{AI05-0022-1} Correction: Added a Bounded (Run-Time) Error to cover tampering by generic actual subprograms.

{AI05-0027-1} Correction: Added a Bounded (Run-Time) Error to cover access to finalized set containers.

{AI05-0160-1} Correction: Revised the definition of invalid cursors to cover missing (and new) cases.

{AI05-0265-1} Correction: Defined when a container prohibits tampering in order to more clearly define where the check is made and the exception raised.

{AI12-0111-1} Procedures Union, Intersection, Difference, and Symmeteric_Difference are now defined to tamper with the cursors of the Target parameter. A program which attempts to use one of these operations while tampering is prohibited will raise Program_Error. However, since the operations do modify the container, the effects would have been unpredictable, so this change will likely fix bugs. 

{AI12-0196-1} Correction: Replace_Element is now defined such that it can be used concurrently so long as it operates on different elements. This allows some container operations to be used in parallel without separate synchronization. 

{AI12-0110-1} Corrigendum: Clarified that tampering checks precede all other checks made by a subprogram (but come after those associated with the call).

{AI12-0112-1} Added contracts to this container. This includes describing some of the semantics with pre- and postconditions, rather than English text. Note that the preconditions can be Suppressed (see 11.5).