Version 1.3 of ai12s/ai12-0187-1.txt

Unformatted version of ai12s/ai12-0187-1.txt version 1.3
Other versions for file 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
!priority Medium
!difficulty Hard
!subject Stable properties of abstract data types
!summary
A method of describing stable properties of abstract data types (ADT) is added to Ada.
!problem
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 critical.]
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.
!proposal
[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 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 property names.
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.
The *stable property functions for type T" for a primitive subprogram S of 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. This is likely to be very rare, so we try to ignore the possibility in the rules.
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 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.
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 normal manner.]
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 to.
!wording
** TBD.
!discussion
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 not visible.
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 functions. 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, useless, complexity).
(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 to define.
(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.
!example
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; -- No implicit postcondition here, this is a stable property -- function.
function Mode (File : in File_Type) return Mode_Type with Pre => Is_Open(File) or else raise Status_Error; -- No implicit postcondition here, this is a stable property -- function.
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; -- No implicit postcondition here, both stable property functions -- are named.
[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 postcondition.
...
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;
...
end Ada.Text_IO;
!ASIS
** TBD.
!ACATS test
An ACATS C-Test is needed to check that the new capabilities are supported.
!appendix

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

Nice proposal!

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