Container operation contracts

As described in the Contracts section (Container operation contracts (AI12-0112 ) – see 3.3), expresses the checks to be performed upon entry to a container's subprograms using Ada 2012 preconditions rather than English.

The aspects Nonblocking (AI12-0064-2 – see 2.3) and Global (AI12-0079-3 – see 2.4) are included in the contracts.

The new aspect Allows_Exit (see 4.4, “Loop-body as anonymous procedure” — AI12-0189 below) is applied to the container Iterate procedures.

All container operations now have versions with the container as the first parameter. This allows a more specific global contract to be specified. Thus:

The former has to allow anything to be read as the container is not explicitly identified, whereas the latter does not access any globals. The two parameter version also has the benefit of allowing prefix notation to be used. The new versions include Element, Query_Element, Next and Previous for vectors and lists; Key, Element, Query_Element, Next and (if ordered) Previous for maps; Element, Query_Element, Next and (if ordered) Previous for sets; and Subtree_Node_Count, Element, Query_Element, Next_Sibling and Previous_Sibling for multiway trees. If the cursor points to a different container to the one given, then Program_Error is raised.

Consider the following example:

package String_Indexes is
   new Indefinite_Hashed_Maps (Key_Type => String,
  ...
   My_Index : constant String_Indexes.Map := String_Indexes.Empty_Map;
function Long_Strings_Count
              (The_Index  : String_Indexes.Map;
               Min_Length : Positive) return Natural is
   Count : Natural := 0;
begin
   for My_Cursor in The_Index.Iterate loop
      if String_Indexes.Key (Position =>
                          My_Cursor)'Length >= Min_Length then
         Count := Count + 1;
      end if;
   end loop;
   return Count;
end Long_Strings_Count;

Note the incongruous mixing of OO-style prefix notation in The_Index.Iterate and traditional notation in String_Indexes.Key. In Ada 2022 the latter can be replaced by The_Index.Key, thus allowing the consistent use of prefix notation.

4.2 Container operation contracts