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

Unformatted version of ai12s/ai12-0187-1.txt version 1.7
Other versions for file ai12s/ai12-0187-1.txt

!standard 7.3.3(0)          17-04-05 AI12-0187-1/04
!standard 13.1.1(4/3)
!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 successful 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
Add a type and subprogram aspect Stable_Properties along with class-wide versions.
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).
The aspect determines a list of property functions for each primitive subprogram. 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).
For the details, see the !wording part of this AI.
!wording
[Editor's note: I've put this into Section 7 after type invariants since it is primarily about ADTs and in particular about private types. Arguably, it should instead follow 6.1.1 as it is also primarily about postconditions (in that case, the references to partial views is a forward reference and would require a "(see 7.3)"; otherwise, nothing but the section number would need to be changed).]
Add a new clause:
7.3.3 Stable Properties of a Type
It is usual that some of the characteristics of a data type are unchanged by most of the primitive operations on the type. Such characteristics are called stable properties of the type.
Syntax
type_property_aspect_definition ::= name {, name}
subprogram_property_aspect_definition ::= [not] name {, [not] name}
Static Semantics
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.
For a private type, private extension, or full type that does not have a partial view, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Stable_Properties
This aspect shall be specified by a type_property_aspect_definition; each name shall statically denote a property function of the type. This aspect defines the stable property functions of the associated type.
AARM Discussion: We do not allow this aspect on generic formal types, as it is only meaningful for primitive subprograms and generic formal types have no such subprograms.
AARM Aspect Description for Stable_Properties: A list of functions describing characteristics that usually are unchanged by primitive operations of the type or an individual primitive subprogram.
Stable_Properties'Class
This aspect shall be specified by a type_property_aspect_definition; each name shall statically denote a property function of the type. This aspect defines the class-wide stable property functions of the associated type. 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 Proof: Class-wide inheritance has to be explicitly defined. Here we are not making such a definition, so there is no inheritance. 6.1.1 defines the inheritance of class-wide postconditions.
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.
AARM Aspect Description for Stable_Properties'Class: A list of functions describing characteristics that usually are unchanged by primitive operations of a class of types or a primitive subprogram for such a class.
For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Stable_Properties
This aspect shall be specified by a subprogram_property_aspect_definition; each name shall statically denote a property function of a type for which the associated subprogram is primitive.
Stable_Properties'Class
This aspect shall be specified by a subprogram_property_aspect_definition; each name shall statically denote a property function of a tagged type for which the associated subprogram is primitive. Redundant[Unlike most class-wide aspects, Stable_Properties'Class is not inherited by descendant subprograms, but the enhanced class-wide postconditions are inherited in the normal manner.]
AARM Reason: The subprogram versions of Stable_Properties are provided to allow overriding the stable properties of a type for an individual primitive subprogram. While they can be used even if the type has no stable properties, that is not an intended use (as simply modifying the postcondition directly makes more sense for something that only happens in one place).
Legality Rules
In a subprogram_property_aspect_definition for a subprogram S:
* all or none of the items shall be preceded by /not/;
AARM Ramification: The listed functions all have /not/ or none
do; mixing /not/ functions with regular functions is not allowed.
* any property functions mentioned after /not/ shall be a stable property function of a type for which S is primitive.
Static Semantics
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".
A similar definition applies for class-wide stable property functions by replacing aspect Stable_Properties with aspect Stable_Properties'Class in the above definition.
The explicit specific postcondition expression for a subprogram S is the expression directly specified for S with the Post aspect. Similarly, the explicit specific postcondition expression for a subprogram S is the expression directly specified for S with the Post'Class aspect.
For every primitive subprogram S of a type T that is not a stable property function of T, the specific postcondition expression of S is modified to include expressions of the form F(P) = F(P)'Old, all /and/ed with each other and any explicit specific postcondition expression, where F is each stable property function of S for type T that does not occur in the explicit specific postcondition expression of S, and P is each parameter of S that has type T. The resulting specific postcondition expression of S is used in place of the explicit specific postcondition expression of S Redundant[ when interpreting the meaning of the postcondition as defined in 6.1.1].
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 specific postcondition is evaluated as described in 6.1.1. One hopes that compilers can be smart enough to prove that many of these added postcondition subexpressions cannot fail, but that is not required here. End AARM Ramification.
For every primitive subprogram S of a type T that is not a stable property function of T, the class-wide postcondition expression of S is modified to include expressions of the form F(P) = F(P)'Old, all /and/ed with each other and any explicit class-wide postcondition expression, where F is each class-wide stable property function of S for type T that does not occur in any class-wide postcondition expression that applies to S, and P is each parameter of S that has type T. The resulting class-wide postcondition expression of S is used in place of the explicit class-wide postcondition expression of S Redundant[when interpreting the meaning of the postcondition as defined in 6.1.1].
AARM Reason: We suppress stable property expressions if the property function appears in the explicit class-wide postcondition, or in any inherited class-wide postconditions. If we didn't do that, we could have conflicting requirements in an inherited postcondition and the current one. We also avoid redundant property checks.
AARM Ramification: The resulting class-wide postcondition is evaluated as described in 6.1.1. In particular, the enhanced class-wide postcondition IS the class-wide postcondition for S, and therefore inherited postconditions include any stable property expressions.
Modify 13.1.1(4/3):
aspect_definition ::= name | expression | identifier | type_property_aspect_definition | subprogram_property_aspect_definition
!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 extra 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, 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.
(9) I didn't make any attempt to modify the wording in 6.1.1 to mention that the class-wide postcondition that "applies" to a subprogram might have been modified to add some stable property expressions. In general, we want to use the same rules for all evaluations of a class-wide postcondition, including any added parts. However, it would appear that this might cause failures of the Legality Rules 6.1.1(10/3-17/3). I believe that the wording is sufficient as I have presented it here, but it is hard to be sure.
!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 in the explicit postcondition.
[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;
...
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.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, December 28, 2016  6:42 PM

Just in time for some light New Year's reading, following find a fully worded
version of the Stable Properties AI.

We did not discuss this AI in Pittsburgh (even though it addresses one of the
"areas of special interest") as it was crowded out by lower-priority AIs.
(Grumble.) I had previously passed an earlier draft past Tucker, and he had
encouraged me to complete the wording. I've now done that, hopefully we won't
now decide to change the model 180 degrees.

As always comments welcome.

[Following was version /03 of the AI - Editor.]

****************************************************************

From: Tucker Taft
Sent: Wednesday, December 28, 2016  6:42 PM

Looks pretty good.  There are some places where I might suggests tweaks to the
wording to improve clarity.  My biggest concern is probably the relatively
informal definition of "actual postcondition."  There seems to be some pretty
significant hand-waving going on there. ;-)

****************************************************************

From: Randy Brukardt
Sent: Thursday, December 29, 2016  6:08 PM

I fully expect "tweaks to the wording", but it's a bit of a disappointment to
only find out that they're needed without anything more specific.

I discussed the need for "hand-waving" in item (9) of the discussion. 6.1.1 is
a jar of wiggly worms which for the moment has the lid on. Removing the lid
seems like a bad idea, since I have no trouble finding many things in that
wording that are inconsistent. (At the risk of loosening the lid that I'd
rather leave in place, two examples are the use of "associated expression"
in 6.1.1(18/5) while all other wording uses some form of "applies"; and the
inconsistent use of "postcondition" and "postcondition expression" in the
wording.)

As such, what is going on is going to require some hand-waving, since the
model is that we're adding stuff to the specific (or class-wide) postcondition
(expression??).

We could get quite specific and write the rules based on the (specific or
class-wide) postcondition expression, but I'm not sure that helps much other
than adding verbiage (especially as then it is necessary to define "explicit
(specific or class-wide) postcondition expression" in order to avoid a
circular definition):

   The *explicit* specific postcondition expression for a subprogram S is the
   expression directly specified for S with the Post aspect. Similarly, the
   *explicit* specific postcondition expression for a subprogram S is the
   expression directly specified for S with the Post'Class aspect. 

   For every primitive subprogram S of a type T that is not a stable property
   function of T, the specific postcondition expression of S is modified to
   include expressions of the form F(P) = F(P)'Old, all /and/ed with each other
   and any explicit specific postcondition expression, where F is each stable
   property function of S for type T that does not occur in the explicit
   specific postcondition expression of S, and P is each parameter of S that
   has type T. The resulting specific postcondition expression of S is used
   in place of the explicit specific postcondition expression of S Redundant[
   when interpreting the meaning of the postcondition as defined in 6.1.1].

[The last redundant part is already in an AARM note, perhaps it should stay
only there??]

And similarly for the class-wide version:

   For every primitive subprogram S of a type T that is not a stable property
   function of T, the class-wide postcondition expression of S is modified to
   include expressions of the form F(P) = F(P)'Old, all /and/ed with each other
   and any explicit class-wide postcondition expression, where F is each
   class-wide stable property function of S for type T that does not occur in
   any class-wide postcondition expression that applies to S, and P is each
   parameter of S that has type T. The resulting class-wide postcondition
   expression of S is used in place of the explicit class-wide postcondition
   expression of S Redundant[when interpreting the meaning of the postcondition
   as defined in 6.1.1].

Is this the sort of thing you meant? Or was there some other problem??

****************************************************************

From: Tucker Taft
Sent: Thursday, December 29, 2016  11:12 PM

> I fully expect "tweaks to the wording", but it's a bit of a 
> disappointment to only find out that they're needed without anything more
> specific.

I will provide more precise suggestions later, but right now I am occupied
with many year-end duties.

> ...
> Is this the sort of thing you meant? Or was there some other problem??

Yes, something along the lines you suggested in this reply would definitely
help me, at least, feel better about the proposal.

****************************************************************

From: Randy Brukardt
Sent: Thursday, December 29, 2016  11:53 PM

> I will provide more precise suggestions later, but right now I am 
> occupied with many year-end duties.

So was I, the main one making sure that I exhausted my 2016 ARG budget.
Having just successfully accomplished that task, I'll have to wait until
next week to apply these changes to the draft.

Happy New Year to all!!!

****************************************************************

From: Randy Brukardt
Sent: Wednesday, April 5, 2017  9:38 PM

> I will provide more precise suggestions later, but right now 
> I am occupied with many year-end duties.

I wonder if "later" has arrived yet. I'd hope that you're done with your
year-end duties by now. ;-) [Hopefully, the quarter-end duties, too.]

>> ...
>> Is this the sort of thing you meant? Or was there some other problem??
>
>Yes, something along the lines you suggested in this reply would definitely
>help me, at least, feel better about the proposal.

I've just applied and posted a revised version of the AI with these changes
made.

(I'll note that I promised to do that "next week" on Dec 29, so you're not
the only one who can put off things indefinitely. ;-)

***************************************************************

Questions? Ask the ACAA Technical Agent