search

Ada-Rapporteur-Group / User-Community-Input

Ada User Community Input Working Group - Github Mirror Prototype
27 stars 1 forks source link

Ada.Containers.Hashed_Sets.Generic_Keys.Find: Error in Postcondition #49

Closed Richard-Wai closed 1 year ago

Richard-Wai commented 1 year ago

@ARG-Editor My apologies if this has already been raised, but I don't recall it.

In Ada 2022 Draft 35 of the RM, I casually spotted an error in the Postcondition for the Generic_Keys.Find function for Hashed_Sets, specifically this is A.18.8(56/5).

Post => (if Find'Result = No_Element then Has_Element (Container, Find'Result))

Obviously this is incorrect, but I also note that the general postcondition for Generic_Keys.Find for all sets at A.18.7(80/5) has the correct postcondition. It seems the '=' should be '/='.

The postcondition is also correct in Ordered_Sets.

ARG-Editor commented 1 year ago

This issue is addressed in AI22-0074-1; that AI is now ARG approved.