!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 is subtle enough, without complicating the issue more by making it depend on
where and how the call is made.]

!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.

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