3.3 Contracts for container operations

Container operation contracts (AI12-0112 ) specifies the checks to be performed upon entry to a container's subprograms. These are now expressed using Ada 2012 preconditions rather than English.

Checking of the preconditions by the containers' users can be suppressed using:

pragma Suppress (Containers_Assertion_Check);

The aspects Nonblocking (AI12-0064-2). and Global (AI12-0079-3). are included in the contracts. Some postconditions are added for "easy" results (such as a requirement that a parameter be empty on return). Postconditions on language-defined operations are required to succeed (otherwise the implementation is wrong! – AI12-0179).