Version 1.2 of ai12s/ai12-0187-1.txt
!standard 7.3.3(0) 16-06-02 AI12-0187-1/01
!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 problem; my car's oil may be
stable, but I still change it periodically. Anyway, better names are surely
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 libraries);
* 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 probably needs wordsmithing.]
Add a type aspect Stable_Properties.
This aspect can be given on a partial view or on a full type with no partial view.
(It's not allowed on formal types, since it is only meaningful for primitive
The value of the aspect is a list of function names. The named functions must
be property functions.
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
For every primitive subprogram S of a type T that is not a stable property
function of T and whose the (explicit) postcondition
does not mention one of the stable property functions 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 type T, and P is each parameter of S that has type T.
AARM Ramification: Any mention of any single property function will cause all of
the properties to be excluded from the postcondition. In that case, the
postcondition ought mention appropriate rules for all of the properties.
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 and two parameters of type T, then there
are six such subexpressions appended to the postcondition.
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.
There ought to be a similar aspect Stable_Properties'Class. This is the same
except that it is inherited by extensions (and thus applies to primitives of
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 as a set. I did that because
in almost every example I looked at, there 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 is 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
I considered making this a user choice (perhaps by separating the function
names by "and" and "or" in order to indicate grouped and separate properties),
but that seemed to add complexity and I didn't find many instances where
separate properties would really work.
(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
(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 conditions. 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.
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 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, but surely
(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
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 Put(File : in File_Type; Item : in String)
with Pre => Mode(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