AI22-0074-1

!standard A.18.8(56/5)                                    23-06-02  AI22-0074-1/01

!class binding interpretation  23-06-02

!status Amendment 1-2022  23-06-27

!status WG9 Approved 23-10-12

!status ARG Approved  6-0-0  23-06-11

!status work item 23-06-02

!status received 23-05-27

!submitter Richard Wai

!priority Low

!difficulty Easy

!qualifier Error

!subject Postcondition error in Ada.Containers.Hashed_Sets

!summary

The postcondition of Ada.Containers.Generic_Keys.Find is corrected.

!issue

The definition of Generic_Keys.Find function for Hashed_Sets, A.18.8(56/5), reads:

function Find (Container : Set;
               Key       : Key_Type)
         return Cursor
         with Post => (if Find'Result = No_Element
                       then Has_Element (Container, Find'Result));

This postcondition does not match that for the operation definition in A.18.7(80/5). It also doesn’t make any logical sense; the “=” should be “/=”.

!recommendation

Correct the operator in the postcondition.

!wording

Modify A.18.8(56/5):

function Find (Container : Set;
               Key       : Key_Type)
         return Cursor
         with Post => (if Find'Result {/=}[=] No_Element
                       then Has_Element (Container, Find'Result));

!discussion

As noted in the !issue, the operation definition (as well as the version in Ordered_Sets) uses “/=”. As such, this mistake appears to be a simple typo.

Since this typo changes the meaning of the expression significantly, we have to process this change as a Binding Interpretation (this does not qualify as a presentation change).

!corrigendum A.18.8(56/5)

@drepl

@xcode{      @b{function} Find (Container : Set;

                     Key       : Key_Type)
        @b{return} Cursor
        @b{with} Post => (@b{if} Find'Result = No_Element
                      @b{then} Has_Element (Container, Find'Result));}

@dby

@xcode{      @b{function} Find (Container : Set;

                     Key       : Key_Type)
        @b{return} Cursor
        @b{with} Post => (@b{if} Find'Result /= No_Element
                      @b{then} Has_Element (Container, Find'Result));}

!ACATS test

No additional ACATS tests should be needed. It’s very unlikely anyone would implement the incorrect postcondition, as it would make the subprogram unusable. Any existing tests would assume the correct postcondition (we did not check if there are any such tests).

!appendix

This AI was created from GitHub issue #49 (https://github.com/Ada-Rapporteur-Group/User-Community-Input/issues/49).