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

Unformatted version of ai12s/ai12-0187-1.txt version 1.2
Other versions for file 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
!priority Medium
!difficulty Hard
!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 welcome.]
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 subprograms.)
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 Stable_Properties.
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 those extensions).
** TBD.
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 not visible.
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 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 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, 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 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 no further.
(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.
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, a stable property function -- is 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 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;
** TBD.
!ACATS test
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

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