Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
Overview of Ada 2022
Jeff Cousins
Contents   Index   Search   Previous   Next 

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.

Contents   Index   Search   Previous   Next 
© 2021, 2022 Jeff Cousins