Overview of Ada 2022
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).
© 2021, 2022 Jeff Cousins