!standard 7.3.2(0)                              11-06-15    AI05-0250-1/01
!class Amendment 11-06-15
!status work item 11-06-15
!status received 11-06-15
!priority Low
!difficulty Easy
!subject Thoughts on type invariants.
!summary

TBD.

!question

1) It would be useful to have the option of specifying the Invariant aspect with
   the full declaration of the type instead of only at the declaration of the
   partial view of the type. It's bizarre to have to make the invariant visible
   to all clients; if often only relevant to the implementation of the type.

2) It would be useful if some mechanism existed for statically enforcing a
   requirement that an invariant expression must not have side effects or, more
   generally, must be "well behaved" (definition details TBD, but this might
   include prohibitions on reading variables and/or on propagating exceptions).

3) It would be useful if the language made a distinction between "internal"
   calls (where the caller is already inside the implementation of the type in
   question) and "external" calls. No runtime invariant checking should be
   performed for an "internal" call.

!proposal

** TBD.

!wording

** TBD.

!discussion

** TBD.

[Editor's note: For (3), the language *does* make such a distinction, but it
makes it between subprograms, not calls. Subprograms declared in the visible
part are external, others are internal. This also seems right: A called
subprogram doesn't know who is its caller, so if it is externally callable, it
needs to ensure the invariant is true on return.

The mail from Yannick Moy suggests that this is in fact the correct solution. So
we probably want no action on (3).]

!ACATS test

** TBD.

!appendix

From: Steve Baird
Sent: Wednesday, June 15, 2011  4:24 PM

An AdaCore customer has identified three issues with Ada 2012's type invariants. I'm passing these along so that the ARG can decide for each whether
   a) some action is needed for Ada 2012; or
   b) some action is needed, but not for Ada 2012; or
   c) no action is needed.

====

1) It would be useful to have the option of specifying the Invariant aspect with
the full declaration of the type instead of only at the declaration of the
partial view of the type.

If what the user really wants is

    package Pkg is
       type Stack is private;
       <exported operations on type T>
    private
       type Stack is record
          Max, Current : Index := 0;
          ...;
       end record with Invariant => Stack.Current <= Stack.Max;
    end Pkg;

, it is annoying to have to write

    package Pkg is
      type Stack is private with Invariant => Is_Valid (T);
      <exported operations on type T>
      function Is_Valid (X : Stack) return Boolean;
    private
       type Stack is record
          Max, Current : Index:= 0;
          ...;
       end record;

       function Is_Valid (X : T) return Boolean is
         (X.Current <= X.Max);
    end Pkg;

, thereby adding an unwanted visible operation (Is_Valid) to the interface. If a
user chooses to think of the invariant as an implementation detail, not part of
the public interface (and not part of a contract which clients need to be aware
of), then that user doesn't want to see any mention of the invariant in the
visible part.

Introducing the Is_Valid function (albeit a function whose completion is an
expression_function) may also have interactions with issue #2 (below).

====

2) It would be useful if some mechanism existed for statically enforcing a
requirement that an invariant expression must not have side effects or, more
generally, must be "well behaved" (definition details TBD, but this might
include prohibitions on reading variables and/or on propagating exceptions).

A new language-defined restriction which only allows "well behaved" invariant
expressions could address this issue.

Concern was also expressed about the particular case of an invariant expression
whose evaluation leads to infinite recursion because the expression itself
contains some construct whose evaluation requires evaluation of the invariant
expression (e.g., due to a type conversion or to a call to a function with an
out-mode parameter).

Hopefully the as-yet-uninvented restriction would catch this case.

====

3) It would be useful if the language made a distinction between "internal"
calls (where the caller is already inside the implementation of the type in
question) and "external" calls. No runtime invariant checking should be
performed for an "internal" call.

The concern here is correctness, not performance.
Inside the implementation, it is perfectly reasonable to
(temporarily) violate a type's invariant. An invariant check performed while
"the hood is up" can be a problem.

One (partial) workaround is to implement each exported operation Foo as a rename
of a non-exported Foo_Implementation subprogram. "Internal" callers who want to
call Foo then call Foo_Implementation instead. Or the private type in question
could be implemented as a derived type with invariant-breaking operations
performed using the non-exported parent type and then only converting to the
exported type when the invariant has been restored.

Either of these approaches is cumbersome.

=====

My own opinions:

    #1 I can see the argument for this. I would not
         be opposed to allowing the Invariant spec to
         be supplied as part of either the private
         type declaration (as it is today) or the
         completion.

    #2 Defining a new restriction for folks who want
         more restrictions on invariant expressions
         seems reasonable, but lots of details TBD.

    #3 The AI currently says
           The invariant checks performed on a call are determined by the
           subprogram or entry actually invoked, whether directly, as
           part of a dispatching call, or as part of a call through an
           access-to-subprogram value.

         There are good reasons for this rule and I think messing with
         it would lead to problems.

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

From: Randy Brukardt
Sent: Wednesday, June 15, 2011  5:00 PM

...
>     #2 Defining a new restriction for folks who want
>          more restrictions on invariant expressions
>          seems reasonable, but lots of details TBD.

Such a restriction makes perfect sense, and should apply to all contracts (that
is, preconditions, postconditions, and subtype predicates) but in the past when
I've proposed such things I've not gotten any traction. I suspect that this is
an area where an implementer needs to take the lead (I definitely will do
something on this like in Janus/Ada should I ever get to implementing contracts,
but obviously something AdaCore does will have a lot more impact).

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

From: Edmond Schonberg
Sent: Wednesday, June 15, 2011  5:10 PM

> ...
>>    #2 Defining a new restriction for folks who want
>>         more restrictions on invariant expressions
>>         seems reasonable, but lots of details TBD.
>
> Such a restriction makes perfect sense, and should apply to all
> contracts (that is, preconditions, postconditions, and subtype
> predicates) but in the past when I've proposed such things I've not
> gotten any traction. I suspect that this is an area where an
> implementer needs to take the lead (I definitely will do something on
> this like in Janus/Ada should I ever get to implementing contracts,
> but obviously something AdaCore does will have a lot more impact).


There have been several  user suggestions along those lines, so we will
definitely introduce such a restriction.  Implementation seems straightforward
if the definition is tight enough. Should there be a pragma (sorry, an aspect)
that asserts that the body of a function satisfies this restriction? They seem
to go together.

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

From: Randy Brukardt
Sent: Wednesday, June 15, 2011  6:17 PM

> > ...
> >>    #2 Defining a new restriction for folks who want
> >>         more restrictions on invariant expressions
> >>         seems reasonable, but lots of details TBD.
> >
> > Such a restriction makes perfect sense, and should apply to all
> > contracts (that is, preconditions, postconditions, and subtype
> > predicates) but in the past when I've proposed such things I've not
> > gotten any traction. I suspect that this is an area where an
> > implementer needs to take the lead (I definitely will do something
> > on this like in Janus/Ada should I ever get to implementing
> > contracts, but obviously something AdaCore does will have a lot more impact).
>
> There have been several  user suggestions along those lines, so we
> will definitely introduce such a restriction.
> Implementation seems straightforward if the definition is tight
> enough. Should there be a pragma (sorry, an aspect) that asserts that
> the body of a function satisfies this restriction? They seem to go
> together.

Yes, I think that is required in order to support separate compilation (and
dispatching, in class-wide contracts). The question of course is whether this
enforces restrictions on the body, and what those restrictions are in that case.
This was one of the purposes of the global in/global out annotations, after all:
a restriction on the global in/global out allowed in functions called from
contract expressions would be easy to specify and enforce. But of course that
depends on the full global in/global out mechanisms. Something more limited in
scope would be easier to define, inplement, and most likely use.

In any case, something to talk about at the meeting. Probably best as a post-Ada
2012 feature, but something that we can scope out anytime as implementations can
add their own aspects and restrictions (so there is no pressing rush).

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

From: Randy Brukardt
Sent: Wednesday, June 15, 2011  6:21 PM

...
>     #3 The AI currently says
>            The invariant checks performed on a call are determined by the
>            subprogram or entry actually invoked, whether directly, as
>            part of a dispatching call, or as part of a call through an
>            access-to-subprogram value.
>
>          There are good reasons for this rule and I think messing with
>          it would lead to problems.

Right. Keep in mind that AI05-0247-1 modifies these rules slightly, to ensure
that inherited routines enforce all of the invariants (including ones the
original body does not know about).

In any case, I'll make a skeleton AI to hold this mail so we have something to
discuss at the meeting next week.

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

From: Tucker Taft
Sent: Wednesday, June 15, 2011  8:37 PM

It certainly makes perfect sense to make the Invariant private, since it is
really something to support the implementation, not the client.

As far as restrictions, that seems not worth standardizing at this point, and I
would expect good compilers to provide warnings without any effort on the part
of the user if the invariant has side-effects or other weirdness.

Distinguishing internal from external calls seems to be more trouble than it is
worth.  The called subprogram doesn't know who is its caller, so if it is
externally callable, it pretty much needs to ensure the invariant is true on
return.  Inlining can be a way of dealing with this without any extra language
support, for the unusual case where it is needed.

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

From: Robert Dewar
Sent: Thursday, June 16, 2011  4:39 AM

...
> As far as restrictions, that seems not worth standardizing at this
> point, and I would expect good compilers to provide warnings without
> any effort on the part of the user if the invariant has side-effects
> or other weirdness.

I agree, let implementations respond to actual usage and suggestions and needs
of users, standardize next time around if appropriate.

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

From: Yannick Moy
Sent: Thursday, June 16, 2011  2:42 AM

> 3) It would be useful if the language made a distinction between
> "internal" calls (where the caller is already inside the
> implementation of the type in question) and "external" calls. No
> runtime invariant checking should be performed for an "internal" call.

Indeed, this is what the customer initially suggested, based on his experience
with Eiffel and C++:

- In Eiffel, it is the syntactic difference between a qualified call "a.f(...)"
  and an unqualified call "f(...)" (called from a method on the implicit
  "Current") that decides whether the invariant is checked or not. It is not
  checked at all on unqualified calls. It is checked on both entry and exit from
  qualified calls.

- For C++, the customer developed their own implementation of C++ macros which
  implement almost fully the rules of design by contract:
  - during evaluation of assertions, the function is executed without evaluation
    of the associated assertions (valid for all assertions)
  - during an internal call, the invariant is not assessed.
The distinction between internal and external calls is implemented with a simple
imbrication counter in the implicit attributes of all objects: if the
imbrication counter is > 1 during a call, the invariant is not evaluated.

But in the conversation that follows, I explained that the distinction between
internal and external *calls* is not appropriate. Rather, we should distinguish
internal and external *subprograms*. What I mean is the following. Suppose you
want to verify formally code that respects the policy of Eiffel. So every
routine over type T can be called either in a context in which the invariant of
T holds, in which case it must reestablish the invariant at the end, or in a
context in which the invariant of T does not hold. This means that every routine
has really *two* different contracts... well, not really. Some routines will be
called only in a context in which the invariant holds, and they may rely on
this, so that they do not execute properly if called in a context in which the
invariant does not hold. So in the end you don't know really whether a routine
should work only in a context in which the invariant holds, or always.

If you perform runtime checking, that's not a problem, because the dynamic
environment tells you in which case you are. But if you aim at formal
verification, you are left with no other choice than ask the user to provide
this information. Since we aim at both with Ada 2012, I much prefer a rule which
states exactly which routines expect to be called in a context in which the
invariant holds. We agreed that such a rule is to check invariants only on
public operations of a type, not on private subprograms (either declared in
private part or in body). So that's this rule that I would like the ARG to
consider.

On 16/06/2011 03:36, Tucker Taft wrote:

> Distinguishing internal from external calls seems to be more trouble
> than it is worth.  The called subprogram doesn't know who is its
> caller, so if it is externally callable, it pretty much needs to
> ensure the invariant is true on return.  Inlining can be a way of
> dealing with this without any extra language support, for the unusual
> case where it is needed.

As explained above, this issue is rather external vs. internal *subprograms*.

Without this distinction, the customer says invariants are "unusable" in his
context. Note that this customer uses pre- and postconditions (pragmas)
extensively (AdaCore developed these for them). My experience is that languages
that do not have a distinction of this kind lead to unusable invariants:

- in Spec# (C#), it is the user responsibility to "open" and "close" objects,
  with the invariant being checked on entry/exit of a call only when the caller
  object is "closed". Very heavy.

- in JML (Java), the invariant is required to hold on entry/exit of every call.
  As a result, invariants are almost not used; people prefer using pre- and
  postconditions.

What would be the problem with this (simple) rule enforcing invariant only on
external subprograms?

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

From: Yannick Moy
Sent: Thursday, June 16, 2011  8:34 AM

> As explained above, this issue is rather external vs. internal *subprograms*.

Our customer pointed us today to the following sentence in B. Meyer's book
"Object-Oriented Software Construction 2nd edition", p 366 under "Who must
preserve the invariant?":

"As a consequence, the obligation to maintain the invariant applies only to the
body of features that are exported either generally or selectively; a secret
feature - one that is available to no client - is not affected by the
invariant."

So Eiffel already has this policy of checking the invariant only on external
*subprograms*, plus it has the internal/external *call* difference. I believe
Ada could implement only the first one, and it would be enough to satisfy the
needs expressed so far.

Ideally, a renaming-as-body of a private operation into a public one would add
the verification of the invariant if necessary:

spec:
  type T is ... with Invariant => Inv(T);
  procedure External (X : out T);  --  Inv(X) checked on exit

body:
  procedure Internal (X : out T);  --  no invariant checking
  procedure External (X : out T) renames Internal;  --  adds Inv(X) checking

which would give an easy way to use an operation both externally (with invariant
checked) and internally (no check).

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

From: Randy Brukardt
Sent: Thursday, June 16, 2011  12:08 PM

...
> What would be the problem with this (simple) rule enforcing invariant
> only on external subprograms?

There is no problem -- it is ALREADY the rule for Type_Invariants in Ada 2012.

Specifically, 7.3.2(12-5/3) [the number is from the working draft of the
Standard, not sure what it was in Draft 11] says about when an invariant is
checked:

Upon return from a call on any subprogram or entry that:

     * has a result of type T, or one or more in out or out parameters of type
       T,

     * is explicitly declared within the immediate scope of type T (or is a part
       of an instance of a generic unit declared within the immediate scope of
       type T), and

     * is visible outside the immediate scope of type T or overrides an
       operation that is visible outside the immediate scope of T,

Note that the last part requires the routine to be one that is visible to
clients; it excludes private operations unless they are overriding some visible
inherited routine.

So the rule you are suggesting is in fact the rule Ada 2012 requires. If your
description of the problem is correct, then we need to do nothing. (Whether GNAT
properly implements these rules is another question, but irrelevant to the ARG.)

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

From: Tucker Taft
Sent: Thursday, June 16, 2011  4:34 PM

> ... What would be the problem with this (simple) rule enforcing
> invariant only on external subprograms?

As Randy pointed out, this is exactly what Ada 2012 does.

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

From: Randy Brukardt
Sent: Thursday, June 16, 2011  6:54 PM

But thanks for confirming that we have it right already. It's one less thing to
worry about. :-)

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

From: Randy Brukardt
Sent: Thursday, June 16, 2011  7:05 PM

...
> As far as restrictions, that seems not worth standardizing at this
> point, and I would expect good compilers to provide warnings without
> any effort on the part of the user if the invariant has side-effects
> or other weirdness.

Well, I surely agree that it is too late for any such restrictions in Ada 2012.

But I don't think it is practical to produce warnings for "bad" contract
expressions; you could only catch some low-hanging fruit and I have to wonder if
such warnings would actually be harmful (by giving a false sense of security).

But such warnings aren't possible if the "bad" things occur within called
functions; expression functions help a bit, but can provide no help for
class-wide contracts as the calls are all dispatching. And as Bob has repeatedly
noted, banning all functions other than expression functions and predefined
operators really isn't practical (especially in the class-wide cases). We really
need some sort of function categorization aspect (or global in/global out
aspects), and that would work with the warnings and/or restrictions to fully
cover the needs.

I do expect AdaCore to end up taking the lead on this, because they clearly have
customer requests for this functionality and they will need to convince the
entire ARG of what is needed (as I have). That's both good and bad (good because
something will actually get done here, bad because the result is likely to be
whatever is easiest for GNAT rather than technically best), but I don't think it
can be helped.

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

From: Yannick Moy
Sent: Friday, June 17, 2011  2:01 AM

>>> ... What would be the problem with this (simple) rule enforcing 
>>> invariant only on external subprograms?
> 
>> As Randy pointed out, this is exactly what Ada 2012 does.
> 
> But thanks for confirming that we have it right already. It's one less 
> thing to worry about. :-)

thanks for the good news that I'll transmit with pleasure to our customer!

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