Version 1.5 of ai12s/ai12-0187-1.txt
!standard 7.3.3(0) 16-08-31 AI12-0187-1/02
!class Amendment 16-06-02
!status work item 16-06-02
!status received 16-06-02
!subject Stable properties of abstract data types
A method of describing stable properties of abstract data types (ADT)
is added to Ada.
It is common that there are properties of an abstract data type (ADT) that
usually don't change during the life of an object of that type. In particular,
most operations on the ADT do not change these properties. For the purposes
of this description, we'll call these "stable properties" of the type.
[Author's note: This term is the result of a trip to the thesaurus. My
original idea was "usually invariant properties", which is both too long and
"invariant" already has a meaning. "Immutable" and "constant" also have been
used, plus all of those need the prefix "usually" to weaken them. "Stable"
doesn't seem to suffer from either of these problems; my car's oil may be
stable, but I still change it periodically. Anyway, the exact name isn't
For instance, for I/O, the open status of a file and the mode of a file are
stable properties (only being changed by a few routines: Open, Create, Close,
Delete, and Reset). For a container, the length and capacity are stable
properties. For a window manager, the visibility, size, position, and color
of a window are stable properties (there probably are more).
Stable properties are important as they can often be determined by simple
program analysis. For instance, after a call to Create, it's obvious that
the file is open and that does not need to be checked on subsequent calls
to I/O routines. For this analysis to be possible, the compiler has to know
that calls to most I/O routines do not change the stable properties.
That can be done in Ada 2012 by including the stable properties in every
postcondition for routines that operate on the ADT. For Text_IO, this would
look something like:
procedure Put_Line (File : in File_Type; Str : in String)
with Pre => Mode(File) = In_File,
Post => Mode(File) = Mode(File)'Old;
This works, but has a number of disadvantages:
* One can easily forget the stable properties on some of the routines,
confounding analysis (worse, it's easy to put conflicting properties
on a routine);
* The postconditions get cluttered with information that is not central to
the routine's purpose (indeed, the ARG required the author to remove the
stable properties from proposed postconditions for the containers
* This can require a lot of extra text, harming readability.
[Author's note: This is pseudo-wording; I've described it fairly formally so
that the rules are clear. It wobbles back-and-forth from formal wording style
to an informal description. It definitely will need formal wording (especially
for the definition of the aspects and the syntax of the "not" lists.)]
Add a type and subprogram aspect Stable_Properties.
This aspect can be given on a partial view or on a full type with no partial
view, and on primitive subprograms. (It's not allowed on formal types, since
it is only meaningful for primitive subprograms.) The intent is that the
subprogram version be used to override the type version when necessary; it
is not very useful as a stand-alone aspect (it makes more sense to just modify
the postcondition in that case).
For a type, the value of the aspect is a list of function names. The named
functions must be property functions. For a primitive subprogram, the value
of the aspect is either a list of function names, or a list of items, each being
"not" followed by a function name; again all of the functions need to be names of
AARM Ramification: For a subprogram, the functions all have "not" or none
do; mixing "not" functions with regular functions is not allowed.
AARM Reason: The aspect Stable_Properties for a subprogram provides a way
to override the properties inherited from a type.
A property function of a type T is a function with a single parameter, that
is a primitive operation of T or a function whose parameter is class-wide and
covers T. The return type of a property function is nonlimited.
The *stable property functions" of a type T are those denoted in the aspect
Stable_Properties for T.
For a primitive subprogram S, any property functions mentioned after "not" for
the Stable_Property aspect of S shall be a stable property function of a type
for which S is primitive.
For a primitive subprogram S of a type T, the stable property functions for S for
type T are:
* if S has an aspect Stable_Properties specified that does not include "not",
those functions denoted in the aspect Stable_Properties for S;
* if S has an aspect Stable_Properties specified that includes "not",
those functions denoted in the aspect Stable_Properties for T, excluding
those denoted in the aspect Stable_Properties for S;
* if does not have an aspect Stable_Properties, those functions denoted in
the aspect Stable_Properties for T, if any.
AARM Discussion: A primitive subprogram can be primitive for more than one
type, and thus there can be more than one such set of stable properties
for a subprogram. Thus we say "stable property functions for S for type T".
For every primitive subprogram S of a type T that is not a stable property
function of T, the actual postcondition of S includes expressions of the form
F(P) = F(P)'Old, all "and"ed with each other and any explicit postcondition,
where F is each stable property function of S for type T that does not occur
in the explicit postcondition of S, and P is each parameter of S that has type T.
AARM Ramification: There is one F(P) = F(P)'Old subexpression for every
combination of stable expression function of type T and parameter of type T.
For instance, if there is three stable property functions for type T and two
parameters of type T, then there are six such subexpressions appended to the
The resulting postcondition is evaluated as described in 6.1.1. One hopes
that compilers can be smart enough to prove that many of these
postconditions cannot fail, but that is not required here.
End AARM Ramification.
For tagged types and their primitive subprograms, there is a similar aspect
Stable_Properties'Class. These aspects works exactly like the equivalent
Stable_Properties aspects, except that they modify the class-wide postcondition
rather than the specific postcondition. Redundant[Unlike most class-wide
aspects, Stable_Properties'Class is not inherited by descendant types and
subprograms, but the enhanced class-wide postconditions are inherited in the
AARM Discussion: Since class-wide postconditions are inherited by
descendants, we don't need the stable property functions to be inherited;
if they were, we'd be duplicating the checks, which we don't want. And
we don't want to duplicate any of the rules about class-wide postconditions,
so we just say that the modified postconditions is what those rules apply
A Bairdian free association on this topic:
(1) The question of whether all of these properties should be treated as a set
or individually is answered here by treating them individually.
The original idea was to treat them as a set, as in most examples, here was
some relationship between the properties. Not all of the properties make sense
in all cases.
For instance, for I/O, Mode doesn't make sense if Is_Open is False. Thus,
if Is_Open appears in a postcondition, we don't want Mode to automatically
appear in it. Similarly, the color of a window may not be well-defined if is
However, others thought that would be too inflexible. Rather, we decided to
use a default-and-override pattern, with Stable_Properties being possible on
individual subprogram. An example of how it would be used is given for
procedure Close in the !example below.
(2) I considered allowing more parameters on a property function, so long as
they can be specified by literals or global objects. However, that made the
rules more complex without much benefit, since a user can always wrap a
function that has too many parameters in an expression function. The parameters
have to be global or literal so that the property function can appear in the
postcondition of every primitive routine of the type; they can't depend on
a parameter of the routine as that would insist that every operation has a
second, identical parameter.
(3) I thought about restricting the result types of property functions to
elementary types. Since the semantics of 'Old are well-defined for nonlimited
types, and composite types like complex numbers seem likely to be useful here,
I didn't make any such restrictions. If the result type is controlled, the
effects might be weird, but that's the user's problem. (If that hurts, don't
do that! :-)
(4) I went with the simple rule for postconditions: any mention of any
stable property function in the postcondition turns off the automatic
stable property condition for that function. I could have used a more detailed
rule requiring the stable property function to have a parameter of the type
from the subprogram in question, and even treated the properties differently
if there are multiple such parameters. While that would get better results in
a few cases, it would have been pretty complex and I have been trying to make
this as simple as possible to make it tractable. Moreover, one can always
explicitly include the checks in the explicit postcondition.
I excluded the postconditions of the stable properties functions themselves
for the obvious reason: otherwise, we'd have infinite recursion (or extra,
(5) I considered other rules, but settled on this applying only to primitive
subprograms to avoid surprises. If someone adds a stable property during
maintenance, we don't want to be adding a requirement to some other routine
in some other package written by some other programmer. If that happened,
the other routine could suddenly be forced to follow some requirement that
it didn't know about (quite possibly leading to surprise Assertion_Errors).
The easiest way to see this is to assume that someone decided to enhance
Text_IO with preconditions and postconditions and stable properties for
Is_Open and Mode. If stable properties applied to all parameters of the
type (and not just primitives), then existing user-written routines that
Open and Close file parameters would fail with Assertion_Error!
It might make sense to extend that rule to cover class-wide routines with
parameters of T'Class in the package with the declaration of T. That is
messy enough that I didn't do it.
(6) One could imagine a similar feature for preconditions. However, predicates
already support that need, with the exception of existing code where
compatibility is paramount (like Text_IO). [Using a predicate requires
changing the subtype profile of a subprogram, and that means that operations
that require subtype conformance, like renaming and 'Access for subprograms,
would fail.] Since new Ada features are mainly used in new code anyway,
(which can and should use predicates), it seems unlikely to be useful enough
(7) I understand this idea is related to the idea found within the program
verification community of "frame conditions". Such conditions help set
the "frame", the set of objects potentially modified by an operation.
We could call the aspect "Frame_Conditions" with suitable changes in
terminology. But that doesn't make the meaning very clear (unless, of
course, you are used to program verification terminology). Moreover, the
initial ARG response was that "stable properties" seemed like an appropriate
description. Thus we're sticking with that term.
(8) The real key to this feature is how well this works in practice, for
packages like the containers. It will be used in AI12-0112-1, so we should
have some fully worked out examples.
Using this feature, Text_IO could be written something like:
package Ada.Text_IO is
type File_Type is private
with Stable_Properties => Is_Open, Mode;
type Mode_Type is (In_File, Out_File, Append_File);
function Is_Open (File : in File_Type) return Boolean;
function Mode (File : in File_Type) return Mode_Type
with Pre => Is_Open(File) or else raise Status_Error;
procedure Open (File : in out File_Type;
Mode : in File_Mode;
Name : in String;
Form : in String := "")
with Pre => (not Is_Open(File) or else raise Status_Error),
Post => Is_Open(File) = True and then
Ada.Text_IO.Mode(File) = Mode;
[Author's note: Those who will complain about writing Is_Open = True (and you
know who you are ;-), I wrote it this way to emphasize that the postcondition
is describing the value of the function Is_Open in addition to the property
that the function represents. A fine distinction.]
procedure Close (File : in out File_Type)
with Stable_Properties => not Mode,
Post => Is_Open(File) = False;
-- No implicit postcondition here, Mode was explicitly removed,
-- and Is_Open is used in the explicit postcondition.
procedure Put(File : in File_Type; Item : in String)
with Pre => Mode(File) /= In_File or else Mode_Error;
-- Mode will raise Status_Error if needed.
-- An implicit postcondition here:
-- Post => Is_Open(File) = Is_Open(File)'Old and then
-- Mode(File) = Mode(File)'Old;
An ACATS C-Test is needed to check that the new capabilities are supported.
From: Randy Brukardt
Sent: Thursday, June 2, 2016 10:22 PM
> > Aside: There's a general problem with preconditions/postconditions
> > as to how to declare properties that are unchanged by (most) routines.
> > For instance, for the Vector container, most routines do not change
> > the length. One could imagine adding Container.Length =
> > Container.Length'Old to every postcondition, but that's nasty to
> > read (it adds a lot of clutter). But one needs that information in
> > order to reason about the property without peeking at the body (the
> > compiler or prover has to know that the length is unchanged by
> > calling Element [for instance] in order to propagate its knowledge
> > to a later precondition). Someone had the idea of having a global
> > property that gets added automatically to every postcondition unless
> > the same property is explicitly tested in the postcondition. That
> > would solve the problem, but how to define "same property being
> > explicitly tested" is unclear. Should I try to put together a proposal
> > on these lines??
> Something along those lines seems like a good idea. I have spent some
> time thinking along those lines, but I don't know the right answer(s).
Well, unlike Bob, I'm happy to propose an answer even if I don't know if it
is the right answer. ;-)
The attached proposal [Version /01 of this AI - Ed.] covers all of the example
cases that I've been able to think of. I suspect that it would break down if
someone wanted very many "stable properties", but I'm unsure if the additional
complexity to fix that would be worthwhile (one would have to support some
method of defining subsets of properties that are exclusive).
I apologize for inventing some terminology from air; there very well might be
a term that reasonably covers this, but I have neither the time nor energy to
figure out if others have tried to solve this problem. After all, this idea is
rather a trial balloon to get a discussion started, not necessarily a finished
answer to the problems of the world's Ada programmers.
From: Tucker Taft
Sent: Friday, June 3, 2016 8:44 AM
This is closely related to the notion of "frame conditions" which is a general
problem in program verification. The "frame" is the set of objects or
properties that are potentially affected by an operation. This issue is
discussed a bit in the Wikipedia article titled "frame problem." Unfortunately
this Wikipedia article is not as helpful as it could be.
We should also relate this to the "Global" aspect, and perhaps consider adding
a "Modified" aspect which would effectively establish a frame condition.
From: Tullio Vardanega
Sent: Friday, June 3, 2016 8:48 AM
Yes, I second.
Questions? Ask the ACAA Technical Agent