Overview of Ada 2022
3.5 Stable properties
Stable properties of abstract
data types (AI12-0187)
adds the new aspect
Stable_Properties (see
RM
7.3.4)
to simplify the description of properties of an abstract data type (ADT),
by making it easy to specify properties that are usually unchanged by
most of the operations of the ADT. The classic example is the Mode of
a file, which is unchanged by all of the operations other than
Create/Open/Close/Reset
(and
Set_Mode for streams). The stable properties
are automatically included in the postconditions of all the primitive
operations of the ADT, decreasing clutter and increasing the information
that provers can use.
The aspect Stable_Properties
can be given on a partial view or on a full type with no partial view,
and also on primitive subprograms. The subprogram version can be used
to override the type version when necessary for specific primitive subprograms
of the type. The aspect is also applicable to class-wide versions.
The aspect is followed by a list of the stable property
functions
(comma-separated if
more than one) for the primitive subprogram(s).
Syntax for Stable_Properties
aspects (AI12-0285)
tweaks the syntax so that the list is enclosed by round brackets, in
the form of a positional aggregate, to avoid possible ambiguity in a
list of aspects.
The postcondition(s) of the subprogram are modified
with an item that verifies that the property is unchanged for each parameter
of the appropriate type, unless that property is already referenced in
the explicit postcondition (or inherited postcondition, in the case of
class-wide postconditions).
To expand on the example
of the Mode of a file, suppose that we wish
many subprograms to behave as if they have a postcondition as in:
procedure Put (File : in File_Type; Str : in String)
with Pre => Mode(File) /= In_File,
Post => Mode(File) = Mode(File)'Old;
Then rather than having
to repeat this postcondition for numerous subprograms, if Ada.Text_IO
could be rewritten in the form:
package Ada.Text_IO is
type File_Type is private
with Stable_Properties => (Is_Open, Mode);
...
then the declaration of Put could simply be:
procedure Put (File : in File_Type; Item : in String)
with Pre => Mode(File) /= In_File;
since we have stated that the Mode is a stable property.
© 2021, 2022 Jeff Cousins
