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

Unformatted version of ai12s/ai12-0044-1.txt version 1.3
Other versions for file ai12s/ai12-0044-1.txt

!standard 7.3.2(19/3)          12-12-01 AI12-0044-1/01
!class binding interpretation 12-12-01
!status work item 12-12-01
!status received 12-09-10
!priority High
!difficulty Medium
!subject Calling visible functions from type invariant expressions
!summary
** TBD.
!question
AI05-0289-1 extends invariant checking to "in" parameters. However, this makes it impossible to call a public function of the type from an invariant expression, as that public function will attempt to check the invariant, resulting in infinite recursion.
For Type_Invariant'Class, which is required to be visible, it is almost impossible to write a useful invariant without calling a public function.
Is it intended that invariants be useless? (No.)
!recommendation
(See summary.)
!wording
** TBD.
!discussion
The easiest fix to this problem is to revert to not checking "in" parameters (that is, to repeal AI05-0289-1). However, this is not appealing for two reasons:
(1) The holes that AI05-0289-1 was intended to plug would be reopened.
These were considered important enough to make a last-minute change to the Standard, it's hard to imagine how they would have gotten less important in 9 months.
(2) The final Ada 2012 Standard (and presumably the printed editions that
will be coming out soon) say that "in" parameters are checked. To change this via an AI would cause an endless line of "bug" reports to implementers about their "incorrect" implementation. The visibility of AIs is quite low within the Ada community and it is unlikely that most users would be aware of such a major change.
A better solution is to somehow mark public subprograms that do not need or want invariant checks, combined with a rule that any direct calls from an invariant expression must be so marked.
A number of possible ways to mark routines have been suggested:
(A) A aspect on the subprogram specification that specifies that no invariant
checks will be made for any type for which the subprogram is primitive. This includes all kinds of parameters. A suggested name is Do_Not_Check_Invariant.
(B) A aspect on the subprogram specification that specifies that no invariant
checks are needed for any type for which the subprogram is primitive. This includes all kinds of parameters. A suggested name is Unmodified_Parameters. [Note that this is subtly different than (A); this aspect asserts that the parameters of the primitive types are not modified, actually or logically. Compilers could warn if the parameters appear to be modified. By "logically" here, we mean that if the parameters are handles or contain handles, the target(s) of those handles are not modified either.] This aspect would be most useful on query and predicate functions, which are the most likely kinds to be used in invariant expression.
(C) A aspect on the subprogram specification that specifies that no invariant
checks are needed for "in" parameters of any type for which the subprogram is primitive. This is the same as (B), except that it only applies to "in" parameters. A suggested name: Unmodified_In_Parameters. [The original suggestion was to mark subprograms that need such checks, but that's backwards for Ada: "safe"/"checked" should be the default. I've turned it around here.]
(D) Invariant checks are not made on functions that are completed with
expression functions in the same package specification. (Such functions have almost no way to modify their parameters that would not already check the invariant.)
(E) Invariant checks are not performed on parameters that are declared
with a special subtype. Extending 'Base for this situation is one suggestion.
(F) Add a marker to types which do not contain handles or access values
that are expected to be modified. This is really a property of the invariant expression more than of the type. A suggested name would be Simple_Invariant. [The original suggestion was to mark types that need such checks, but that's backwards for Ada: "safe"/"checked" should be the default. I've turned it around here. Either way, it is not a complete solution; one of the other ideas would be needed as well.]
Note that the legality rule only applies directly within the invariant expression; we make no attempt to prove that any calls made from within the marked functions are OK (that is, don't make invariant checks themselves). That's especially important if the marking mechanism is automatic somehow, [ideas (D) and (F) in particular] as it is likely that routines that are not going to be used in an invariant expression will be involved.
[Editor's musing: The root problem here, IMHO, is that Ada doesn't have any way to tell between a parameter that is intended to be read-only vs. a parameter that is going to be modified somehow ("modified" here means a deep modification of anything that is logically part of the object). For instance, type File_Type in Text_IO is an "in" parameter to Put, but Put changes the line/column counters in the object, and probably has other effects on the object. The object has mode "in", but it still is being modified. OTOH, function Name also has an "in" parameter, but it is just a query function and it is very unlikely that the associated object is modified in any way. The "best" solution to this problem is to have a way to mark the difference between these situations, in which case only routines that don't modify their parameters can be used in invariant expressions. (This also would help the performance of invariants markedly.)
Note that I don't like the 'Base solution (E), or the aspect (A) (I know it was my idea, bear with me!) because they put the emphasis on the wrong property: the presence of the check. I think the emphasis should be placed on describing when the invariant check cannot be needed -- this is safer because it only introduces a hole when the programmer is claiming the check isn't needed -- rather than just suppressing the check.]
!ACATS test
An ACATS x-Test should be created to test these rules.
!appendix

From: Tucker Taft
Sent: Monday, September 10, 2012  11:07 AM

Here is another ARG issue identified by Yannick Moy.
The problem is that we decided to check Type_Invariants on "in" parameters, to
handle cases where a private type involves a level of indirection, as with
Text_IO's File_Type.  But checking "in" parameters creates a problem when the
Type_Invariant itself calls a visible function with an "in" parameter, which it
almost certainly will.

Totally non-obvious to me how to deal with this, other than to go back to only checking IN-OUT and OUT parameters, and leaving a hole for IN parameters.  Trying to "suspend"
type-invariant checks while evaluating a type invariant is very difficult to implement in its full generality, I suspect.

>>> I think that RM 7.3.2.19/3 is missing a restriction to OUT and IN
>>> OUT parameters. ...
>> See AI05-0289.
>>
>> The !summary section consists of only:
>> Invariants are checked on all parameters of the type after a call,
>> including "in" parameters.
>>
>> So, for better or for worse, the present wording was a deliberate
>> choice and not an oversight.
>
> We'd better think about a modification of the RM right now then,
> because there is no way to create an interesting type invariant that is
> not recursive:
>
> type T is private with Type_Invariant => Public_Function (T);
>
> function Public_Function (X : T) return Boolean;
>
> If the type invariant is checked when returning from Public_Function,
> we've got a problem...
>
> Plus I'm sure I raised this issue on the ARG mailing list and we
> agreed during the discussion the invariant would only be checked for OUT and
> IN OUT parameters.

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

From: Robert Dewar
Sent: Monday, September 10, 2012  11:20 AM

Perhaps we can work out something less than full generality which would
represent a best compromise here.

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

From: Yannick Moy
Sent: Monday, September 10, 2012  11:23 AM

> Here is another ARG issue identified by Yannick Moy.
> The problem is that we decided to check Type_Invariants on "in"
> parameters, to handle cases where a private type involves a level of
> indirection, as with Text_IO's File_Type.

I don't understand how this applies to File_Type, which is typically implemented
as an access. This is already taken care of explicitly in the RM.

> But checking "in" parameters creates a problem when the Type_Invariant
> itself calls a visible function with an "in"
> parameter, which it almost certainly will.
>
> Totally non-obvious to me how to deal with this, other than to go back
> to only checking IN-OUT and OUT parameters, and leaving a hole for IN
> parameters.

You could have the check for IN parameters of access type, is it the case you
had in mind when changing the RM? Or is it something more subtle having to do
with access discriminants (the Rosen trick)?

>  Trying to "suspend"
> type-invariant checks while evaluating a type invariant is very
> difficult to implement in its full generality, I suspect.

Plus we want something easy to understand and explain. Not something which is
enabled/disabled depending on the dynamic calling context.

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

From: Tucker Taft
Sent: Monday, September 10, 2012  11:37 AM

>> Here is another ARG issue identified by Yannick Moy.
>> The problem is that we decided to check Type_Invariants on "in"
>> parameters, to handle cases where a private type involves a level of
>> indirection, as with Text_IO's File_Type.
>
> I don't understand how this applies to File_Type, which is typically
> implemented as an access. This is already taken care of explicitly in the RM.

Not sure what you mean by this.  File_Type might be a record type, but with a
component which is of an access type.

> You could have the check for IN parameters of access type, is it the
> case you had in mind when changing the RM? Or is it something more
> subtle having to do with access discriminants (the Rosen trick)?

The private type might be completed with a record type, with one or more
subcomponents which were of an access type. Or the private type might be an
index into a global table. If the type-invariant looks "through" that index,
then clearly it might be violated by a function that takes an IN parameter, if
the function updates the table.

But we know there are holes, so it is probably better to revert to the
IN-OUT/OUT parameter check only, than create some complex mechanism to deal with
IN parameters.

>> Trying to "suspend"
>> type-invariant checks while evaluating a type invariant is very
>> difficult to implement in its full generality, I suspect.
>
> Plus we want something easy to understand and explain. Not something
> which is enabled/disabled depending on the dynamic calling context.

Agreed.

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

From: Robert Dewar
Sent: Monday, September 10, 2012  1:35 PM

How complex would it be to just exempt calls to functions with in parameters
where the call appears within a contract expression?

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

From: Tucker Taft
Sent: Monday, September 10, 2012  1:49 PM

That doesn't really work since the function you call directly might call another
public function indirectly, and that would result in recursion.  I think better
is to make the "standard" policy check IN-OUT and OUT parameters only, and then
allow implementations to provide a "stricter" policy which might do more
(hopefully somewhat intelligently).

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

From: Robert Dewar
Sent: Monday, September 10, 2012  2:00 PM

Well you could just avoid this by avoiding such calls to public functions. But
you can't avoid the outer level call, since it has to be visible.

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

From: Erhard Ploedereder
Sent: Tuesday, September 11, 2012  9:11 AM

I would have assumed that calls on primitive functions inside a type-invariant
are "inner calls" where the type-invariant is not checked at all. (As far as a
model goes, the type-invariant is like a primitive routine invoked from the
outside; its contents are/can be inner calls.) If this is not so, it should be.

to which Tuck says implicitly:
> That doesn't really work since the function you call directly might
> call another public function indirectly, and that would result in
> recursion.

As would a type_invariant on an OUT parameter that calls a primitive function
that calls a public procedure with an OUT parameter of the same type. Is that so
much different?

Actually, anytime you call "publically" inside a type-invariant, directly or
indirectly, you are probably in trouble (and not just because of possible
infinite recursions).

I pushed hard for type-invariant checks on "in"-parameters, because the
Rosen-Trick as well as the modifying of indirectly addressed data can destroy
the type-invariant for an "in"-parameter, very much like for an out parameter.

I really objected to anything called a type-invariant, if it can be falsified in
full accordance to language rules. That is not just a small hole, it's a barn
door.

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

From: Robert Dewar
Sent: Tuesday, September 11, 2012  2:23 PM

> I would have assumed that calls on primitive functions inside a
> type-invariant are "inner calls" where the type-invariant is not
> checked at all. (As far as a model goes, the type-invariant is like a
> primitive routine invoked from the outside; its contents are/can be
> inner calls.) If this is not so, it should be.

What do you mean by "inside" here?

Do you mean statically inside? If so, your assumption corresponds to the
suggestion I made

Or do you mean dynamically inside? That's the intepretation that worries Tuck
(and me) as being very hard to implement.

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

From: Erhard Ploedereder
Sent: Tuesday, September 11, 2012  2:45 PM

I meant statically inside. (But there is a visibility issue here, isn't there,
to have direct calls on primitive functions of the type itself.)

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

From: Robert Dewar
Sent: Tuesday, September 11, 2012  3:00 PM

I see no visibility issue? Can you explain, remember that preconditions etc can
have forward referencs.

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

From: Tucker Taft
Sent: Tuesday, September 11, 2012  3:38 PM

And we dropped the notion of "inner calls."  An invariant must be preserved by
any function that *can* be called from outside, and is checked even when called
from "inside." The exception to this is view conversions, which only involve a
check if occurring outside the scope of the full type.

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

From: Erhard Ploedereder
Sent: Tuesday, September 11, 2012  4:01 PM

Shucks. That makes it a rock and a hard place, right?

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

From: Randy Brukardt
Sent: Tuesday, September 18, 2012  1:56 PM

It's not that bad. At least three solutions come to mind that don't involve
giving up on "in" parameter checks. But they need more explanation than I can
give on a cell phone, so that will have to wait until I get home.

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

From: Randy Brukardt
Sent: Tuesday, October 2, 2012  6:39 PM

I wrote from on top of a mountain in Sequoia National Park:

> It's not that bad. At least three solutions come to mind that don't involve
> giving up on in parameter checks. But they need more explanation than I can
> give on a cell phone, so that will have to wait until I get home.

In response to Erhard's:

>> And we dropped the notion of "inner calls."  An invariant must be
>> preserved by any function that *can* be called from outside, and is
>> checked even when called from "inside."
>
>Shucks. That makes it a rock and a hard place, right?

As far as I know, we never had the notion of "inner calls", so we couldn't drop
it. The model has always been that each subprogram operated identically no
matter where it is called, because otherwise no one could ever figure out what
ought to happen (the visibility rules in Ada being beyond the ability of mere
mortals to understand - would we really want invariant checks to be a
"characteristic" and appear and disappear in hard-to-explain ways? I think not).

I should note that I was never really convinced of the need for "in"
parameter checks in the first place; I dropped my opposition mainly because it
was obvious that enough others were convinced and I wanted to move on to more
important problems. I'm writing the following possible rules in order to have
solutions to consider, but I would personally prefer just dropping the checks on
"in" parameters and making it clear that if you don't declare you side-effects
to the outside world, no one is going to help.

So, clearly one choice is simply:

(0) Revert to the original rule of checking "in out" and "out" parameters only.

But let's look at other alternatives.

Let's narrow the problem somewhat. I will postulate that the only place that we
need to avoid invariant checks is in the actual invariant expression. If that
expression calls functions that in their bodies make calls that do invariant
checks, there will be a problem, but it seems impossible to prevent such
problems (given that the bodies can be arbitrarily complex), and such
expressions could never be used in static analysis anyway, so hopefully most
users will avoid these. In any case, if we want to allow some "in" parameter
checks, we're going to have cases of deep inner calls that could end up
recursive (and it probably can happen even if only "in out" parameters are
checks), so it doesn't pay to worry about these cases.

Having done that, what can we say about the invariant expression?

First, we can easily note that any subprogram used directly in an invariant must
be a function. One can call procedures from function bodies, but we've already
decided (above) that we're not going to worry about such cases.

So another choice is:

(1) Check all parameters for procedures, but check only "in out" and "out"
parameters for functions.

One can make an argument that while procedures might modify their arguments (as
the only way to return results), functions doing so without advertising it is
evil. Functions ought to use "in out" parameters when they are going to modify
the parameters. (Yes, this means that I think the random number generator in Ada
is evil. It would be much better written with an "in out" parameter.)

We can find another solution by looking at the "generic" form of this problem.

     type Priv is private
        with Type_Invariant => Invariant(Priv);

     function Invariant (P : in Priv) return Boolean;

The problem in a nutshell is that it is impossible to write this function such
that it is not primitive and visible. (But also see below). Thus, if the
parameter is checked, infinite recursion is sure to result.

We can see that this function always will have to return some boolean type.
So another possible rule immediately appears:

(2) Check only "in out" and "out" parameters for (visible) functions returning a
    boolean type; check all parameters otherwise.

Another option is to have an aspect specifically to suppress in parameter
invariant checks:

(3) Check all parameters unless aspect "Part_of_Invariant_Expression" is used
    (only allowed on boolean functions?), thus:

    function Invariant (P : in Priv) return Boolean
       with Part_of_Invariant_Expression;

Note that in both of these cases, an arbitrary invariant expression can be
handled reorganizing to use an expression function:

That is, replace:
     type Priv is private
        with Type_Invariant => <<expression>>;

with

     type Priv is private
        with Type_Invariant => Invariant(Priv);

     function Invariant (P : in Priv) return Boolean is
        (<<expression>>);

Note that if <<expression>> contains a function call Foo, more rearrangement
will avoid the recursion problem. That is:

     type Priv is private
         with Type_Invariant => ... Foo (Priv) ...;

     function Foo (P : in Priv) return <<something>>;

can be replaced by:

     type Priv is private
        with Type_Invariant => Invariant(Priv);

     function Foo (P : in Priv) return <<something>>;

     function Invariant (P : in Priv) return Boolean;
  private

     function Priv_Foo (P : in Priv) return <<something>>;

     function Foo (P : in Priv) return <<something>> is (Priv_Foo(P));

     function Invariant (P : in Priv) return Boolean is
        (... Priv_Foo (P) ...);

Here, Priv_Foo does not have invariants checked. We then use that in the
Invariant function to avoid recursion.

The fact that this rearrangement is possible provides the last solution:

(4) Make no change to the language. Public invariants are essentially impossible
(but not necessary anyway).

Putting the invariant on the full declaration allows the use of private routines
for which the invariant is not checked.

The problem with (4) is that it doesn't work very will for class-wide invariants
(which we do not allow supplying privately because all extensions of the type
ought to know about the invariant (as it will apply to them, and they cannot
cancel it)).

Which leads to:
(4a) Allow class-wide invariants in the private part.

The reason above is methodological rather than required; but it does mean that
extension writers would always have to peek into the private part to find out
about invariants that might apply.

----

I think that (2) or (3) is the best solution if we think checking "in"
parameters is very important, and (0) is the best solution if we think checking
them isn't that important.

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

From: Yannick Moy
Sent: Wednesday, October 3, 2012  2:19 AM

> I should note that I was never really convinced of the need for "in"
> parameter checks in the first place; I dropped my opposition mainly
> because it was obvious that enough others were convinced and I wanted
> to move on to more important problems. I'm writing the following
> possible rules in order to have solutions to consider, but I would
> personally prefer just dropping the checks on "in" parameters and
> making it clear that if you don't declare you side-effects to the outside
> world, no one is going to help.

I prefer this rule to any other that you mentioned. Like you say, this is a
problem of distinguishing functions with side-effects from functions without
side-effects, so this would be best dealt with a language that supports global
IN, OUT and IN OUT declarations, like SPARK. So best left for a possible future
version of Ada when these annotations are part of the language.

> Let's narrow the problem somewhat. I will postulate that the only
> place that we need to avoid invariant checks is in the actual
> invariant expression. If that expression calls functions that in their
> bodies make calls that do invariant checks, there will be a problem,
> but it seems impossible to prevent such problems (given that the
> bodies can be arbitrarily complex), and such expressions could never
> be used in static analysis anyway

Note that such expressions can be used in formal verification, like we do in the
GNATprove tool developed between AdaCore and Praxis.

> (1) Check all parameters for procedures, but check only "in out" and "out"
> parameters for functions.

Surprising for the user, given the asymmetry.

> (2) Check only "in out" and "out" parameters for (visible) functions
> returning a boolean type; check all parameters otherwise.

Even more asymmetry. Rule is hard to remember, and the workaround that you
propose (put a function not returning a Boolean in the private part, possibly
inserting an indirection if needed) is a burden.

> (3) Check all parameters unless aspect "Part_of_Invariant_Expression"
> is used (only allowed on boolean functions?), thus:

Makes using type invariants too complex.

> (4) Make no change to the language. Public invariants are essentially
> impossible (but not necessary anyway).

Again, this forces an indirection if the actual function called in the invariant
is in the public API.

> I think that (2) or (3) is the best solution if we think checking "in"
> parameters is very important, and (0) is the best solution if we think
> checking them isn't that important.

I think checking invariant on IN parameters is likely to lead to infinite
recursion, because in the body of some function called from the invariant,
another function is called which triggers the invariant again. This largely
out-weights the possible gains from additional checking.

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

From: Randy Brukardt
Sent: Wednesday, October 3, 2012  9:46 PM

...
> > (2) Check only "in out" and "out" parameters for (visible) functions
> > returning a boolean type; check all parameters otherwise.
>
> Even more asymmetry. Rule is hard to remember, and the workaround that
> you propose (put a function not returning a Boolean in the private
> part, possibly inserting an indirection if needed) is a burden.

Sure, but so what? Ada is not designed to make it easy to *write* anything.
Surely we would rather make it harder to write a type invariant rather than
allow a "truck-sized hole" in the checking. (More below.)

> > (3) Check all parameters unless aspect "Part_of_Invariant_Expression"
> > is used (only allowed on boolean functions?), thus:
>
> Makes using type invariants too complex.

See above. Making it easy to write an invariant (or anything else) is not a goal
of Ada. If you tried to craft an argument about readability, it would carry much
more weight.

> > (4) Make no change to the language. Public invariants are
> > essentially impossible (but not necessary anyway).
>
> Again, this forces an indirection if the actual function called in the
> invariant is in the public API.

That's backwards. The indirection is in the function in the public API; the
private function called by the invariant never has an indirection. (You can
never call anything in the public API from an invariant in this model; it's
fairly easy to remember and the workaround isn't that hard.)

> > I think that (2) or (3) is the best solution if we think checking "in"
> > parameters is very important, and (0) is the best solution if we
> > think checking them isn't that important.
>
> I think checking invariant on IN parameters is likely to lead to
> infinite recursion, because in the body of some function called from
> the invariant, another function is called which triggers the invariant
> again. This largely out-weights the possible gains from additional
> checking.

For people that believe that there is a "truck-sized hole" if invariants are not
checked on "in" parameters, any extra effort required to create an invariant is
worthwhile. Ada is certainly not about leaving serious holes in the checking
simply to make it a bit easier to write something uncommon. After all, you'll
write a lot more calls to routines protected by an invariant than you will write
invariants.

Erhard had made a fairly convincing argument that a package structured like
Ada.Text_IO ought to be able to use and enforce invariants. More generally, any
package using handles (as opposed to direct data) ought to be able to use and
enforce invariants. In both cases, a parameter being an "in" parameter does not
tell us anything about whether the invariant might need to be rechecked (because
the backing data structures could have changed).

Erhard didn't convince me with that argument, but he convinced everyone else. It
seems to me that it is silly to throw out that argument simply because it makes
it a bit harder to write an invariant expression. That doesn't seem very
Ada-like to me.

There also is the obvious issue that making such a change (to not check "in"
parameters) would be incompatible with the "published standard", as Tucker put
it in another thread. The incompatibility would only show up in programs that
fail an assertion somewhere, so you can make an argument that it is OK to be
incompatible. But still it would be better to stay as close to the Ada 2012
standard as possible.

Of course, I'm essentially arguing Erhard's position for him. That sometimes
leads down an incorrect path. It would be valuable to hear from him and others
who thought that checking "in" parameters was important, to see what they think
now.

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

From: Jeff Cousins
Sent: Thursday, October 4, 2012  5:19 AM

How about don't check in parameters for any expression functions?

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

From: Yannick Moy
Sent: Thursday, October 4, 2012  5:58 AM

> How about don't check in parameters for any expression functions?

I like this proposal. This is simple, yet does the job of separating functions
which are expected to be called in type invariants and should not have effects
(the expression functions) from functions which may have effects (even on their
IN parameters).

Of course, it might be necessary to have the body of a unit to know whether a
function is implemented as an expression function or not, but that's fine,
because the place where the type invariant is checked should not concern the
user of a unit, but it's implementer.

And it has the nice effect of requiring the use of expression functions
precisely for expressing the properties to check in assertions, which was the
reason for introducing them in the first place. I like this proposal a lot!!!

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

From: Tucker Taft
Sent: Thursday, October 4, 2012  7:53 AM

> How about don't check in parameters for any expression functions?

I agree with Yannick that these kinds of rules are adding complexity without
being a clear solution to the problem.

OK, so here is my attempt to add complexity:

If a subprogram has at least one OUT or IN OUT parameter, then upon return we
check the appropriate invariant on *all* parameters, be they IN, IN-OUT, or OUT.

Since I presume it would be illegal/evil to have an OUT or IN OUT parameter for
a function used to define a type invariant, this would make certain we don't
check any invariants recursively.

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

From: Yannick Moy
Sent: Thursday, October 4, 2012  8:49 AM

>> How about don't check in parameters for any expression functions?
>
> I agree with Yannick that these kinds of rules are adding complexity
> without being a clear solution to the problem.

I found this specific proposal quite interesting on the contrary. (See my
previous email earlier today.)

> OK, so here is my attempt to add complexity:
>
> If a subprogram has at least one OUT or IN OUT parameter, then upon
> return we check the appropriate invariant on *all* parameters, be they
> IN, IN-OUT, or OUT.
>
> Since I presume it would be illegal/evil to have an OUT or IN OUT
> parameter for a function used to define a type invariant, this would
> make certain we don't check any invariants recursively.

I guess this does not solve the issue for Text_IO like units.

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

From: Jeff Cousins
Sent: Thursday, October 4, 2012  9:41 AM

I think that users would see my suggestion as a cleaner split between when in
parameters are checked and when they aren't, expression functions will be
perceived as a different class of things from other subprograms.

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

From: Bob Duff
Sent: Thursday, October 4, 2012  9:49 AM

> OK, so here is my attempt to add complexity:

;-)

> If a subprogram has at least one OUT or IN OUT parameter, then upon
> return we check the appropriate invariant on *all* parameters, be they
> IN, IN-OUT, or OUT.

Clever.  I think I like it.

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  10:09 AM

> I think that users would see my suggestion as a cleaner split between
> when in parameters are checked and when they aren't, expression
> functions will be perceived as a different class of things from other
> subprograms.

I agree, and in fact I think it is very ugly to have OUT or IN OUT parameters
for expression functions :-(

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  10:11 AM

> I think that users would see my suggestion as a cleaner split between
> when in parameters are checked and when they aren't, expression
> functions will be perceived as a different class of things from other
> subprograms.

I actually think that expression functions should be required to be clearly pure
(the arguments about memo functions etc really do not apply here), and even
though the language does not require this, I think it is good style, and may
consider adding a style switch to GNAT to enforce this view.

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  10:12 AM

>> If a subprogram has at least one OUT or IN OUT parameter, then upon
>> return we check the appropriate invariant on *all* parameters, be
>> they IN, IN-OUT, or OUT.
>
> Clever.  I think I like it.

Yes, I think this is a good idea

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

From: Tucker Taft
Sent: Thursday, October 4, 2012  10:14 AM

> I found this specific proposal quite interesting on the contrary. (See
> my previous email earlier today.)

I didn't see any earlier message from you today.  I saw your message from
yesterday.

>> OK, so here is my attempt to add complexity:
>>
>> If a subprogram has at least one OUT or IN OUT parameter, then upon
>> return we check the appropriate invariant on *all* parameters, be
>> they IN, IN-OUT, or OUT.
>>
>> Since I presume it would be illegal/evil to have an OUT or IN OUT
>> parameter for a function used to define a type invariant, this would
>> make certain we don't check any invariants recursively.
>
> I guess this does not solve the issue for Text_IO like units.

It helps somewhat, since many of these have [IN] OUT parameters.

If we made it check *all* invariants on all procedure calls and on function
calls with [IN] OUT parameters, we would probably catch all of the interesting
Text_IO operations.

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

From: Bob Duff
Sent: Thursday, October 4, 2012  10:31 AM

> I actually think that expression functions should be required to be
> clearly pure (the arguments about memo functions etc really do not
> apply here), and even though the language does not require this, I
> think it is good style, and may consider adding a style switch to GNAT
> to enforce this view.

You can't enforce it without outlawing calls to normal functions.

I'm not sure I agree that it's good style.  Why shouldn't I call Cosine from an
expression function?  And why shouldn't Cosine memo-ize?

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  10:33 AM

> You can't enforce it without outlawing calls to normal functions.

Why is that? I just check that expression meets the requirements for a pure
function???

> I'm not sure I agree that it's good style.  Why shouldn't I call
> Cosine from an expression function?  And why shouldn't Cosine
> memo-ize?

Because it's not that much of a burden in practice to write a normal function in
this case (after all Ada up to now has required this for *all* functions).

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

From: Bob Duff
Sent: Thursday, October 4, 2012 10:57 AM

> Why is that? I just check that expression meets the requirements for a
> pure function???

Yes, you're right -- you could do that.

> > I'm not sure I agree that it's good style.  Why shouldn't I call
> > Cosine from an expression function?  And why shouldn't Cosine
> > memo-ize?
>
> Because it's not that much of a burden in practice to write a normal
> function in this case (after all Ada up to now has required this for
> *all* functions).

I don't see how that's relevant.  You said impure expression functions are poor
style, without explaining why they're poor style. The fact that there's an easy
workaround (write a function body) doesn't tell me why they're evil in the first
place.

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  11:13 AM

Because to me, expression functions feel like pure functions it seems very odd
for instance for them to have an IN OUT parameter.

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

From: Randy Brukardt
Sent: Thursday, October 4, 2012  12:41 PM

...which they can't even (directly) modify (as they have no assignment).
They could pass an IN OUT parameter to some other function with an IN OUT
parameter, but that's about it.

When I proposed them, I imagined them as pure and always inlined. We didn't
require either of those things, but I would expect the vast majority of them to
qualify.

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  1:25 PM

> ...which they can't even (directly) modify (as they have no assignment).
> They could pass an IN OUT parameter to some other function with an IN
> OUT parameter, but that's about it.

Right, you really have to work to have IN OUT parameters that are actually changed. That's why I find it odd.
>
> When I proposed them, I imagined them as pure and always inlined. We
> didn't require either of those things, but I would expect the vast
> majority of them to qualify.

ditto!

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

From: Bob Duff
Sent: Thursday, October 4, 2012  2:35 PM

> Because to me, expression functions feel like pure functions it seems
> very odd for instance for them to have an IN OUT parameter.

I think you're saying you don't like impure expression functions because you
just don't like them -- in other words, it's a matter of taste for you.  That's
a perfectly reasonable opinion, but I think expert opinions should be taken as
weaker arguments than facts and reasons.

Here's a fact:  If you require expression functions to be pure, then changing a
function from non-memo-izing to memo-izing is not a compatible change (callers
might have to change).

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  2:40 PM

> I think you're saying you don't like impure expression functions
> because you just don't like them -- in other words, it's a matter of
> taste for you.  That's a perfectly reasonable opinion, but I think
> expert opinions should be taken as weaker arguments than facts and
> reasons.

Well matters of taste are what style switches are about (remember that's what I
was suggesting!)

> Here's a fact:  If you require expression functions to be pure, then
> changing a function from non-memo-izing to memo-izing is not a
> compatible change (callers might have to change).

Don't understand that, can you explain?

P.S. I still find it strange to have in out parameters in expression functions!

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

From: Bob Duff
Sent: Thursday, October 4, 2012  2:54 PM

> Well matters of taste are what style switches are about (remember
> that's what I was suggesting!)

Fair enough.  I probably wouldn't even mind using that, so long as I get to
suppress the warning once in a while.

But I don't see how the solution to this issue (Type_Invariant and "in"
parameters) can be based on any style switches.

> > Here's a fact:  If you require expression functions to be pure, then
> > changing a function from non-memo-izing to memo-izing is not a
> > compatible change (callers might have to change).
>
> Don't understand that, can you explain?

Suppose F is a regular old function with a body, no pragma Pure, but also no
side effects. And suppose you call it from an expression function. (I think that
will be common -- Tucker gave a good example.) Then if you change F to be
memo-izing, you will have to change the expression function.

But you pointed out above that "require expression functions to be pure"
isn't what you meant -- it's just a warning, and warnings are suppressable.

We should probably quit all this talk about warnings here -- that's GNAT
specific, and not entirely appropriate for an ARG discussion.

> P.S. I still find it strange to have in out parameters in expression
> functions!

Sure, so do I.  I also find it strange to have 'in out' params on regular old
functions with bodies.  I want to be able to do it, but only once in a while.
Most functions really ought to be pure.  Even if you can't say pragma Pure, as
for memo-izing functions, they should be conceptually pure.

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  3:01 PM

> But I don't see how the solution to this issue (Type_Invariant and
> "in" parameters) can be based on any style switches.

It's not based on the style switches but on the thought behind them. If in
general this view of expression functions appeals to a lot of people, then it's
not terrible to have the language rule about checking parameters follow this
rule.

It seems rare enough to need to check in parameters in expressin functions, and
rare enough to have IN OUT or OUT parameters for expression functions that
having to write a body if you do need these checks is not a significant
hardship!

>>> Here's a fact:  If you require expression functions to be pure, then
>>> changing a function from non-memo-izing to memo-izing is not a
>>> compatible change (callers might have to change).
>>
>> Don't understand that, can you explain?
>
> Suppose F is a regular old function with a body, no pragma Pure, but
> also no side effects.
> And suppose you call it from an expression function.
> (I think that will be common -- Tucker gave a good example.) Then if
> you change F to be memo-izing, you will have to change the expression
> function.

Yes, but that's not incompatible for callers, you just change it to have a body,
which does not affect the callers, so I still don't get it!

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

From: Bob Duff
Sent: Thursday, October 4, 2012  3:13 PM

> It's not based on the style switches but on the thought behind them.
> If in general this view of expression functions appeals to a lot of
> people, then it's not terrible to have the language rule about
> checking parameters follow this rule.

OK, if it's a style rule that I'm allowed to break once in a while, then yes,
this view of expression functions appeals to me.

> > Suppose F is a regular old function with a body, no pragma Pure, but
> > also no side effects.
> > And suppose you call it from an expression function.
> > (I think that will be common -- Tucker gave a good example.) Then if
> > you change F to be memo-izing, you will have to change the
> > expression function.
>
> Yes, but that's not incompatible for callers, you just change it to
> have a body, which does not affect the callers, so I still don't get
> it!

The caller I'm talking about is the caller of F.

F is in some package.  The expression function is in some other package that is
a client of the first package. It would be nice if you could change F without
changing its caller.

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

From: Randy Brukardt
Sent: Thursday, October 4, 2012  12:37 PM

> I didn't see any earlier message from you today.  I saw your message
> from yesterday.

Yannick's mail is getting moderated (presumably he hasn't sent enough messages to qualify for the "free pass", or his sending address doesn't match his subscription address), so I have to approve it. Given that he's sending his messages in the middle of th
e night my time, that delays them quite a bit).

> >> OK, so here is my attempt to add complexity:
> >>
> >> If a subprogram has at least one OUT or IN OUT parameter, then upon
> >> return we check the appropriate invariant on *all* parameters, be
> >> they IN, IN-OUT, or OUT.
> >>
> >> Since I presume it would be illegal/evil to have an OUT or IN OUT
> >> parameter for a function used to define a type invariant, this would
> >> make certain we don't check any invariants recursively.
> >
> > I guess this does not solve the issue for Text_IO like units.

Yannick beat me to this. I was going to say that your rule would exclude Put and
Put_Line. If you had an invariant involving the line and column counters, that
would leave it unchecked in far too many cases.

> It helps somewhat, since many of these have [IN] OUT parameters.
>
> If we made it check *all* invariants on all procedure calls and on
> function calls with [IN] OUT parameters, we would probably catch all
> of the interesting Text_IO operations.

And I was going to suggest the above as a fix. Great minds and all of that.

But I think I kind of prefer the expression function rule suggested elsewhere.
Although I'm not quite sure how it would work when the expression function is
given in the package body and is the completion of a declaration from the
specification. In that case, the reader couldn't see that it was unchecked.
OTOH, as Robert notes, impure expression functions are likely to be pretty rare
(they could only occur if the function calls something impure or with "in out"
parameters, as no assignments are possible inside of the expression). So maybe
it's OK to suppress the checks even if the body is invisible.

And I was actually leaning toward the "aspect" solution, because it changes the
least. But the expression function solution is nearly as good.

It should be noted that any routines that an expression function calls still
would have checks if public, so the dual private/public routines I had suggested
still might be needed in some cases. As I noted yesterday, this doesn't bother
me because ease of writing isn't a goal of Ada.

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

From: Tucker Taft
Sent: Thursday, October 4, 2012  1:17 PM

>> How about don't check in parameters for any expression functions?
> ... And it has the nice effect of requiring the use of expression
> functions precisely for expressing the properties to check in
> assertions, which was the reason for introducing them in the first place. I like this proposal a lot!!!

I don't. ;-)

I don't see why an invariant should imply use of an expression function.
Also, it seems quite possible that even though the invariant might be defined by
a call on an expression function, the expression might turn around and call a
non-expression function.  E.g.:

     ... with Type_Invariant => Is_Valid(T);

    function Is_Valid(X : T) return Boolean is (Width(X) in 0..Max_Width);

where Width is an out-of-line function.

You are going to force all of the functionality required to establish validity
into expression functions.  That could be a big disruption on existing code,
making it harder to add Type_Invariant to existing abstractions.

In my view, many invariants are going to be completely private to the
implementation, and there is no need to expose them at all to the client, nor
expose all of their functionality in the private part.

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

From: Robert Dewar
Sent: Thursday, October 4, 2012  1:24 PM

>> How about don't check in parameters for any expression functions?
>
> I like this proposal. This is simple, yet does the job of separating
> functions which are expected to be called in type invariants and
> should not have effects (the expression functions) from functions
> which may have effects (even on their IN parameters).
>
> Of course, it might be necessary to have the body of a unit to know
> whether a function is implemented as an expression function or not,
> but that's fine, because the place where the type invariant is checked
> should not concern the user of a unit, but it's implementer.
>
> And it has the nice effect of requiring the use of expression
> functions precisely for expressing the properties to check in
> assertions, which was the reason for introducing them in the first
> place. I like this proposal a lot!!!

I agree, this proposal also makes sense to me

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

From: Randy Brukardt
Sent: Thursday, October 4, 2012  3:16 PM

> You are going to force all of the functionality required to establish
> validity into expression functions.  That could be a big disruption on
> existing code, making it harder to add Type_Invariant to existing
> abstractions.

Not at all. You can always call private functions from the invariant code, and
as I showed on Monday, it's easy to make a private version of a public function.

> In my view, many invariants are going to be completely private to the
> implementation, and there is no need to expose them at all to the
> client, nor expose all of their functionality in the private part.

If they're completely private, the issue never arises, because we don't check
invariants on private subprograms. Ever. The issue only arises when calling
*public* functions from an invariant, and the solution mainly is to call private
versions instead. But we have to have some solution for the top-level function
(which necessarily has to be public), and the expression function idea works as
well as any other proposed.

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

From: Erhard Ploedereder
Sent: Thursday, October 4, 2012  7:13 PM

I'd still have a semantic rather than a "syntactic" rule, partly because all the
rules discussed so far have a "fragile feel" to them, partly because it is hard
to rationalize them froma user perspective.

How about: "A type invariant check on an object succeeds trivially if invoked
during a type invariant check on this object."

The run-time protocol would look like:
 if currently_checked_object = this then null;  else
    declare old_cco: object := currently_checked_object;
    begin
      currently_checked_object := this;
      <do the type invariant check on this>
      currently_checked_object := old_cco;
    end;
  end if;

(It is not a 100%-proof rule, but it is much harder to see the hole that the
rule has in theory.)

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

From: Randy Brukardt
Sent: Thursday, October 4, 2012  8:50 PM

> How about: "A type invariant check on an object succeeds trivially if
> invoked during a type invariant check on this object."
>
> The run-time protocol would look like:
>  if currently_checked_object = this then null;  else
>     declare old_cco: object := currently_checked_object;
>     begin
>       currently_checked_object := this;
>       <do the type invariant check on this>
>       currently_checked_object := old_cco;
>     end;
>   end if;

That's a lot of overhead for the common case that a routine is not called from
the invariant. And it's certainly not possible in general to determine whether
that happens (if an invariant calls a routine defined elsewhere, there is no way
for the compiler to tell if that routine uses the public interface of the
package in any way). My main objection to checking "in" parameters is that it
increases the overhead of checking by many times; this idea would also have such
a multipler.

I think a fully static rule is needed so we're not making checking much more
expensive to fix an unusual case; if you don't like any of the rules based on
the profile or body, surely a rule based on an aspect is acceptable? (The
compiler could even warn if a public routine is called from the invariant that
doesn't have the aspect -- although that's true for all of the other ideas as
well.)

Note that a rule based on an aspect definitely has a clear user case: if you
plan to call a public routine from an invariant expression, it needs the aspect.
And the aspect clearly declares the intentional hole.

(Humm, I suppose you could combine your idea and my aspect idea to eliminate the
hole altogether, and only force the overhead on routines that need it, although
I think that is overkill.)

BTW, I'm unconvinced that you actually can implement the above: "this" isn't
well-defined for by-copy types (like an access type), and a private type surely
can have a full type which is such a type.

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

From: Tucker Taft
Sent: Thursday, October 4, 2012  9:36 PM

> How about: "A type invariant check on an object succeeds trivially if
> invoked during a type invariant check on this object."

Let's not forget multitasking!

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

From: Geert Bosch
Sent: Thursday, October 4, 2012  10:24 PM

> Of course, I'm essentially arguing Erhard's position for him. That
> sometimes leads down an incorrect path. It would be valuable to hear
> from him and others who thought that checking "in" parameters was
> important, to see what they think now.

Maybe the rule should be that type invariants should be checked for IN
parameters if they have limited types. After all, these are the types that one
uses for the Rosen trick with references to variable views.

Incidentally, these also correspond to the File_Type and Generator types where
subprograms take IN parameters of these types and modify them.

In order to prevent recursive calls on the invariant checking routines, it
probably would make sense to have a separate entry points (or wrapper functions)
for the variants that performs invariant checks and the ones that don't. This
seems more like an implementation nuisance than a fundamental problem.

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

From: Randy Brukardt
Sent: Friday, October 5, 2012  12:14 AM

...
> In order to prevent recursive calls on the invariant checking
> routines, it probably would make sense to have a separate entry points
> (or wrapper functions) for the variants that performs invariant checks
> and the ones that don't. This seems more like an implementation
> nuisance than a fundamental problem.

I've been suggesting that be done explicitly since my message Monday. Trying to
do it automatically is full of problems: when do you call the unchecked version
and when do you call the checked version? We looked at options for doing that
early on, and nothing looked very appealing.

Using an unchecked version only when called directly from an invariant
expression might work, but it wouldn't fix much (a lot of functions call other
functions, which would still be checked), and more importantly would be a large
implementation burden (it would require context-dependent code generation for
expressions, something not necessary currently, plus every public routine would
need two versions in case it was called from a type invariant - we've "proved"
the Erhard's suggestion wouldn't work, so only a wrapper could work). There also
would be a small overhead in the normal case (as the checking would have to be
in the wrapper, thus an extra level of calls would be required for the normal
checked calls). All told, I don't think this idea is very appealing.

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

From: Yannick Moy
Sent: Friday, October 5, 2012  2:38 AM

>> You are going to force all of the functionality required to establish
>> validity into expression functions.  That could be a big disruption
>> on existing code, making it harder to add Type_Invariant to existing
>> abstractions.
>
> Not at all. You can always call private functions from the invariant
> code, and as I showed on Monday, it's easy to make a private version
> of a public function.

I was about to say the same thing.

>> In my view, many invariants are going to be completely private to the
>> implementation, and there is no need to expose them at all to the
>> client, nor expose all of their functionality in the private part.
>
> If they're completely private, the issue never arises, because we
> don't check invariants on private subprograms. Ever. The issue only
> arises when calling *public* functions from an invariant, and the
> solution mainly is to call private versions instead. But we have to
> have some solution for the top-level function (which necessarily has
> to be public), and the expression function idea works as well as any other
> proposed.

Given the variety of solutions proposed, I'd like to say that the final solution
should rather be simple than complete. No solution will ever 'close all the
holes'. Even the recent proposal by Geert that only IN parameters of limited
types are checked does not account for cases where the type is just a
(non-limited) index in a global data structure. I see two simple solutions:

- either do not check type invariants on IN parameters;
- or do not check type invariants on IN parameters of expression functions.

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

From: Bob Duff
Sent: Friday, October 5, 2012  8:51 AM

> Let's not forget multitasking!

Yeah.

We talked about following the Eiffel model, which checks at run time "am I
inside the class?" or "am I inside the assertion check?" or something like that.
But we decided it's way too complicated, both implementation-wise and
programmer-wise.

The Eiffel model was invented before Eiffel had multi-threading, by the way.

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

From: Robert Dewar
Sent: Friday, October 5, 2012  9:02 AM

> and more importantly would
> be a large implementation burden (it would require context-dependent
> code generation for expressions, something not necessary currently,

That seems a bogus concern, this seems a trivial implementation issue,
esppecially since we already have context dependent things, like where 'Old is
used.

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

From: Randy Brukardt
Sent: Friday, October 5, 2012  12:54 PM

Huh? I'm talking about context-dependent *code generation*, not legality checks
(these are separate phases in our compiler, and I would expect in most
compilers). 'Old gets generated the same way anywhere it legally appears, it
doesn't depend on context. There is an extra pass to extract and evaluate 'Old
prefixes at the start of the subprogram, but that has nothing to do with the
code generated to evaluate a use of 'Old (it will be a totally separate walk of
the tree, sharing nothing with normal expression code generation).

The only context our compiler uses for code generation is the expected type of
the subexpression. Everything else comes from the resolved symbols in the
expression. I could imagine some solution to context-dependent calls using an
extra tree walk and duplicate symbol table entries, but it is *very* heavy
compared to the actual problem.

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

From: Randy Brukardt
Sent: Friday, October 5, 2012  1:00 PM

...
> Given the variety of solutions proposed, I'd like to say that the
> final solution should rather be simple than complete. No solution will
> ever 'close all the holes'. Even the recent proposal by Geert that
> only IN parameters of limited types are checked does not account for
> cases where the type is just a (non-limited) index in a global data
> structure. I see two simple solutions:
>
> - either do not check type invariants on IN parameters;
> - or do not check type invariants on IN parameters of expression
> functions.

You left out the simplest solution at all: have an aspect to declare that a
routine is used in a type invariant. In which case no invariant checks are done
for the routine; otherwise, the checks are done as specified in the language.

That's more flexible than just limiting to expression functions, and has far
fewer holes than never checking invariants on IN parameters (and would never
cause a hole unintentionally, as the expression function rule might).

No one seems to have seriously considered this idea other than me; that could be because everyone hates it, but no one has said that or tried to explain why. More likely it's because no one noticed the idea.

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

From: Tucker Taft
Sent: Friday, October 5, 2012  1:11 PM

> I see two simple solutions:
>
> - either do not check type invariants on IN parameters;
> - or do not check type invariants on IN parameters of expression functions.

I believe whatever solution we produce should prevent infinite recursion at
compile-time due to type-invariant checks, in all but the most obscure cases.  I
don't think the programmer should have to think about/worry about this problem
at all, and shouldn't have to create wrappers, etc. to avoid infinite recursion.
The programmer should be able to write the most natural and appropriate type
invariant, and it should work as expected.

To me it is much better to omit the check on an IN parameter, than to make
Type_Invariant a burden to use properly.  But perhaps there is some clever
solution which gets the check on most IN parameters without introducing the
recursion for the "typical" situation. (The "expression function" solution
doesn't do it for me because choosing whether or not to use an expression
function seems like an independent decision, and if there are already visible
out-of-line functions that are useful in defining the invariant, duplicating
their logic or moving their logic into an expression function seems an
unnecessary burden on using Type_Invariant.)

For the types that do involve levels of indirection where "IN" mode is
essentially a "lie", the implementor of the abstraction can always add
postconditions to check the invariant explicitly on those few operations that
have this characteristic.  This also reduces the performance burden of
Type_Invariant, by *not* performing it in all of those situations where the "IN"
mode was truthful, and no noticeable change to the state of the object was
occurring.

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

From: Tucker Taft
Sent: Friday, October 5, 2012  1:17 PM

> ... No one seems to have seriously considered this idea other than me;
> that could be because everyone hates it, but no one has said that or
> tried to explain why. More likely it's because no one noticed the idea.

I don't like this idea.  This is adding complexity to Type_Invariant, and
requires you to indicate that an operation is used somewhere in the definition
of a type invariant when that seems potentially irrelevant to the purpose.

What would make more sense to me would be the opposite, that is, identify places
where an "in" parameter is a lie, and hence a Type_Invariant check is desired on
the parameter.

E.g.
     procedure Read(File : File_Type; Item : out Item_Type)
       with Check_Invariant => File;

This provides useful documentation, and if it results in infinite recursion,
then the programmer gets just what they deserve for calling an operation like
"Read" from a Type_Invariant for File_Type.

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

From: Randy Brukardt
Sent: Friday, October 5, 2012  1:40 PM

> I believe whatever solution we produce should prevent infinite
> recursion at compile-time due to type-invariant checks, in all but the
> most obscure cases.  I don't think the programmer should have to think
> about/worry about this problem at all, and shouldn't have to create
> wrappers, etc.
> to avoid infinite recursion.  The programmer should be able to write
> the most natural and appropriate type invariant, and it should work as
> expected.

This is why I find the aspect solution appealing. Add the aspect to any routine
you call from the invariant, and you are done. There is no wrappers required,
and the compiler can warn if you call a routine that doesn't have the aspect.

> To me it is much better to omit the check on an IN parameter, than to
> make Type_Invariant a burden to use properly.  But perhaps there is
> some clever solution which gets the check on most IN parameters
> without introducing the recursion for the "typical" situation.
> (The "expression function" solution doesn't do it for me because
> choosing whether or not to use an expression function seems like an
> independent decision, and if there are already visible out-of-line
> functions that are useful in defining the invariant, duplicating their
> logic or moving their logic into an expression function seems an
> unnecessary burden on using
> Type_Invariant.)

Minor quibble here: neither "duplicating their logic" or "moving their logic
into an expression function" is necessary. Instead, you make a private version
of the routine (with a different name); rename the body to the new name; and
provide an expression function that calls the private version to complete the
public version. This is much better than duplicating the logic (if the logic can
be in an expression function, it probably ought to be there anyway, so that
change is probably for the better).

I expect this construct to be fairly common even without considering the type
invariant expression issue. It's quite common to need to call operations within
the package while the invariant is violated, and calling a public operation in
such a case would cause a bogus invariant failure. So you'll still need the
workaround.

Even so, your original point about the burden of rearranging the code stands.

> For the types that do involve levels of indirection where "IN" mode is
> essentially a "lie", the implementor of the abstraction can always add
> postconditions to check the invariant explicitly on those few
> operations that have this characteristic.  This also reduces the
> performance burden of Type_Invariant, by *not* performing it in all of
> those situations where the "IN" mode was truthful, and no noticeable
> change to the state of the object was occurring.

The whole point of type invariants is to eliminate the error-prone process of
adding explicit checks to postconditions.

You're rehashing all of the arguments that I made (and failed with) in
Stockholm. If it wasn't good enough then, it's surely not good enough now. I
realize that you were on the fence about this argument -- when I lost you on the
topic was when I gave on it. But there were lots of people *not* on the fence,
they didn't buy any of the above from the beginning and I'd be shocked if they
started now. (In addition, the expression function suggestions make it fairly
clear that at least in the case of expression functions, IN mode invariant
checks can be omitted unless the expression function calls a private function
that is not an expression function -- otherwise, it is not possible for the
function to modify its parameters, so no check could possibly fail.)

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

From: Erhard Ploedereder
Sent: Saturday, October 6, 2012  4:47 PM

>> > I'd still have a semantic rather than a "syntactic" rule, partly
>> > because all the rules discussed so far have a "fragile feel" to
>> > them, partly because it is hard to rationalize them froma user
>> > perspective.

> Of course, I'm essentially arguing Erhard's position for him. That
> sometimes leads down an incorrect path. It would be valuable to hear
> from him and others who thought that checking "in" parameters was
> important, to see what they think now.

There are two concerns that I am trying to get resolved:

The infinite recursion:
- I am unsure that not checking "in" parameters solves the infinite
  recursion problem. It solves mostly the case at hand, i.e., a
  simple function call in the type invariant, where the recursion is
  blatently obvious. What if that function calls on procedures that
  do have in out parameters, though? I suspect that "in" parameters
  take the bad rap for a problem that runs much deeper.

The IN parameters:
- I am trying to preserve the notion that a type invariant IS
  GUARANTEED to hold outside of primitive ops. Any model of
  verification that I am aware of is based on this property.
  That's why it is called a type invariant as opposed to
  ocasionally checked type assertion. ;-)
  I would prefer Ada not to be the exception to this rule,
  merely because it is perceived by some to be too expensive to implement.
  That is my main concern in this issue. Whatever solutions are being
  presented, this is my yard stick for being for or against it.
  I do not care so much what the rules will be, but give me that guarantee.
  (When it comes to IN parameters, this is both a question of
   Rosen semantics and of modified indirect hidden components.)

(Aside: I did think about multi-tasking. I presumed the stack to be
thread-local, but failed to write it down.)

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

From: Yannick Moy
Sent: Monday, October 8, 2012  3:03 AM

> What would make more sense to me would be the opposite, that is,
> identify places where an "in" parameter is a lie, and hence a
> Type_Invariant check is desired on the parameter.
>
> E.g.
>      procedure Read(File : File_Type; Item : out Item_Type)
>        with Check_Invariant => File;
>
> This provides useful documentation, and if it results in infinite
> recursion, then the programmer gets just what they deserve for calling
> an operation like "Read" from a Type_Invariant for File_Type.

Like Randy said, this puts the burden on the programmer to annotate each
subprogram with the appropriate aspect. Following your idea, it would be better
to identify the places where a type is not "flat", that is, you can expect that
taking it as an IN parameter still allows modifications of the parameter
(whether through Rosen semantics or modified indirect hidden components, like
Erhard said):

   type File_Type is limited private with
     Check_Invariant_In => True;

The meaning of the above would be: "check the type invariant for each part of an
IN parameter of type File_Type, as if it was an IN OUT parameter".

This does not detect a possible infinite recursion problem due to type
invariants being called, but this problem seems better handled with static
analysis than with a language rule.

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

From: Tucker Taft
Sent: Monday, October 8, 2012  10:07 AM

> The meaning of the above would be: "check the type invariant for each
> part of an IN parameter of type File_Type, as if it was an IN OUT parameter".

The name of the aspect is a bit awkward ;-), but it seems we can agree that the
*default* should be don't check "in" parameters, and only if the programmer
makes it clear that there are levels of indirection should we start checking an
"in" parameter.  Whether it is per-type or per-subprogram seems like a smaller
concern.

I prefer per-subprogram because it clarifies which subprograms take advantage of
the indirection to update the parameter, and which don't.  This is like a "poor
man's" global-in-out annotation.   Perhaps on the subprogram:

    with Modifies => <in_parameter>
  or
    with Modifies => (<in_param1>, <in_param2>, <in_param3>, ...)

which when combined with a Type_Invariant, results in a check on the invariant
upon return from the subprogram on the specified IN parameters.

> This does not detect a possible infinite recursion problem due to type
> invariants being called, but this problem seems better handled with static
> analysis than with a language rule.

The per-subprogram approach *does* solve the infinite recursion problem, which
is the original problem we are trying to solve!

Also, the per-subprogram approach can be combined with some static analysis to
allow the compiler/static-analyzer to complain if you have a Type_Invariant on a
type, and you don't correctly identify the visible operations that modify IN
parameters.

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

From: Bob Duff
Sent: Monday, October 8, 2012  10:28 AM

> I prefer per-subprogram because it clarifies which subprograms take
> advantage of the indirection to update the parameter, and which don't.

But we already have a per-subprogram syntax for that: "in out".
Even better than per-subprogram -- it's per-parameter.

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

From: Yannick Moy
Sent: Monday, October 8, 2012  10:33 AM

> I prefer per-subprogram because it clarifies which subprograms take
> advantage of the indirection to update the parameter, and which don't.
> This
> is like a "poor man's" global-in-out annotation.   Perhaps on the
> subprogram:
>
>     with Modifies => <in_parameter>
>   or
>     with Modifies => (<in_param1>, <in_param2>, <in_param3>, ...)
>
> which when combined with a Type_Invariant, results in a check on the
> invariant upon return from the subprogram on the specified IN parameters.

It seems risky to add such an aspect to Ada 2012 now, given that a lot of
discussion went into the similar AI05-0186 (global-in and global-out
annotations) without reaching a consensus. Maybe the best solution now is to do
nothing, and add checks on IN after adding global aspects to Ada.

>> This does not detect a possible infinite recursion problem due to
>> type invariants being called, but this problem seems better handled
>> with static analysis than with a language rule.
>
> The per-subprogram approach *does* solve the infinite recursion
> problem, which is the original problem we are trying to solve!

How does it solve it? A real solution would have to detect at run-time that the
type invariant is already being checked for the object, before attempting to
check it again.

> Also, the per-subprogram approach can be combined with some static
> analysis to allow the compiler/static-analyzer to complain if you have
> a Type_Invariant on a type, and you don't correctly identify the
> visible operations that modify IN parameters.

This requires having proper aspects for these effect (read/write) annotations, I
think.

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

From: Robert Dewar
Sent: Monday, October 8, 2012  10:30 AM

> The name of the aspect is a bit awkward ;-)

bit awkward????
it's HORRIBLE!

I would just call it Check_Invariants
and let documentation explain the details.

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

From: Robert Dewar
Sent: Monday, October 8, 2012  10:35 AM

>> I prefer per-subprogram because it clarifies which subprograms take
>> advantage of the indirection to update the parameter, and which don't.
>
> But we already have a per-subprogram syntax for that: "in out".
> Even better than per-subprogram -- it's per-parameter.

I agree that labeling such parameters IN OUT is not terrible, yes, it's not
technically accurate, but it's more reflective of what's going on than labeling
them IN and changing them!

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

From: Tucker Taft
Sent: Monday, October 8, 2012  10:46 AM

It is a bit late to change the mode of the File_Type parameters in Get_Line and
Put_Line in Text_IO!

In any case, so long as the default is *not* to check IN parameters for type
invariants, I am happy.  If the programmer has to take some concrete action
(over and above using Type_Invariant, that is) to create the possibility of
infinite recursion, then we can say "caveat emptor."  As it is now, almost *any*
use of Type_Invariant is likely to produce infinite recursion, and that makes
Type_Invariant pretty nearly useless in my view.

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

From: Robert Dewar
Sent: Monday, October 8, 2012  12:04 AM

> It is a bit late to change the mode of the File_Type parameters in
> Get_Line and Put_Line in Text_IO!

Sure, but the issue is much more general than Text_IO, which is little used in serious programs anyway.
>
> In any case, so long as the default is *not* to check IN parameters
> for type invariants, I am happy.  If the programmer has to take some
> concrete action (over and above using Type_Invariant, that is) to
> create the possibility of infinite recursion, then we can say "caveat
> emptor."  As it is now, almost *any* use of Type_Invariant is likely
> to produce infinite recursion, and that makes Type_Invariant pretty
> nearly useless in my view.

Right, I think the default should be not to check!

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

From: Bob Duff
Sent: Monday, October 8, 2012  12:35 PM

> It is a bit late to change the mode of the File_Type parameters in
> Get_Line and Put_Line in Text_IO!

Sure.  If the implementer of Text_IO (or any other existing package that can't
have its interface modified) wants to check invariants on 'in' parameters,
they'll have to do it by hand if we go this route.

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

From: Robert Dewar
Sent: Monday, October 8, 2012  12:39 PM

The likelihood of any implementor doing *anything* with Text_IO is amazingly
minimal! :-)

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

From: Randy Brukardt
Sent: Monday, October 8, 2012   5:53 PM

> I prefer per-subprogram because it clarifies which subprograms take
> advantage of the indirection to update the parameter, and which don't.

I don't. That puts the burden back on the programmer to know where these
modifications might happen. But a significant part of the benefit of
Type_Invariant over Post is that it gets automatically added everywhere it is
needed, even if the programmer doesn't know that it is needed.

It is a property of the invariant expression whether or not it can change via
indirect components, and that is where any extra annotation should be.

(Note, however, that having such an annotation does nothing to fix the recursion
problem; it just limits it to cases with indirect components. I still think we
need separate annotation to mark routines used in invariants; at the very least
for Type_Invariant'Class, whose function call must be public.)

If the real solution to this problem is global in/out annotations, then we
better get back to work on them (I don't want any "poor man's" solution to that
problem - it's far too important for half solutions) -- but I'm very skeptical
that those would help at all.

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

From: Randy Brukardt
Sent: Monday, October 8, 2012  6:29 PM

...
> There are two concerns that I am trying to get resolved:
>
> The infinite recursion:
> - I am unsure that not checking "in" parameters solves the infinite
>   recursion problem. It solves mostly the case at hand, i.e., a
>   simple function call in the type invariant, where the recursion is
>   blatently obvious. What if that function calls on procedures that
>   do have in out parameters, though? I suspect that "in" parameters
>   take the bad rap for a problem that runs much deeper.

This problem is unfixable (in any automatic way).

It can't be fixed dynamically. You had suggested a solution involving wrapping
every check with code like:
   if Current_Invariant /= this then <<Make check>> end if;

But this doesn't work for two reasons:
(1) Tasking. Most packages containing private types are library-level. The
    intent is that the type invariant checks are added automatically to the body
    of these routines. "Current_Invariant" above has to be a per-task global (to
    avoid tasking issues). Since these routines are library-level, a global
    can't be on any stack (there is no stack context passed into library-level
    routines). That only leaves two ways of accessing "Current_Invariant":
    (A) pass it as a parameter to every such routine. That is a nasty
	distributed overhead, also requiring wrappers for uses of 'Access
	(Janus/Ada has to do that for generic sharing, and I wouldn't wish that
	on my worst competitor).
    (B) Make it a task attribute. But the performance of task attributes can be
	slow, and moreover, there is no current requirement that Ada compilers
	even implement them. (And even if they do, they can limit the number and
	size allowed -- C.7.2(29) -- not a theorectical concern -- I had to
	modify the task attribute ACATS tests to allow rejection because some
	existing implementations only allowed a single task attribute.)
(2) Value semantics. Type invariants are allowed on all private types, including
    those completed by by-copy types like integers and access values. In this
    case, "this" is not well-defined, because the object in question is not
    available (or may not even exist) within the subprogram.

To take a concrete example, if a private type is an integer handle, a call from
within the package might pass an expression:
     Do_Something (Handle + 1, ...);
What is "this" for "Handle + 1"? If we simply use the value in these cases,
besides needing a much more complicated definition, we might fail to perform the
check because some old invariant check happened to use the same value. That
doesn't sound good.

So I don't think there is any reliable fix for this problem that would work
dynamically.

A static fix would require that only private routines or those public marked (or
allowed by rule) to be used in invariant expressions. The top level of any such
rule could be checked easily, but what about calls in subprograms called by the
invariant expression? There is no way for a compiler to check such a rule,
unless we adopted a subprogram classification just for invariant expressions,
and disallowed calling anything other than those subprograms from within
themselves. That seems pretty complex and draconian.

A static analysis tool could make such a check, of course, but not an Ada
compiler.

So I think this problem is unfixable. We could adopt one or more rules to
minimize it, but it can't be eliminated.

> The IN parameters:
> - I am trying to preserve the notion that a type invariant IS
>   GUARANTEED to hold outside of primitive ops. Any model of
>   verification that I am aware of is based on this property.
>   That's why it is called a type invariant as opposed to
>   occasionally checked type assertion. ;-)
>   I would prefer Ada not to be the exception to this rule,
>   merely because it is perceived by some to be too expensive
>   to implement.
>   That is my main concern in this issue. Whatever solutions are being
>   presented, this is my yard stick for being for or against it.
>   I do not care so much what the rules will be, but give me
>   that guarantee.
>   (When it comes to IN parameters, this is both a question of
>    Rosen semantics and of modified indirect hidden components.)

This is the crux of the issue. If you believe this, then I don't think anything
that excepts "IN" parameters generally is going to be acceptable. It would have
to be limited to cases where "IN" parameters cannot be modified or by some
explicit exception annotation. The former is the expression function case
previously proposed (it is quite hard to write an expression function that could
modify an "IN" parameter and *not* have it checked somewhere else); the latter
is an annotation asking that a particular function not have "IN" parameters
checked.

Both of these minimize likelihood of hitting the infinite recursion in
"sensible" code, but it can happen. Compilers can sometimes warn about it, and
static analysis tools can always see the problem. The workaround is easy and
will be needed anyway (I think).

What would not be acceptable is having to mark routines that might need "IN"
parameters checked, because that means that the invariant only holds if the
programmer is smart enough to find all of the places that need to be marked.
That doesn't seem like a guarantee to me.

> (Aside: I did think about multi-tasking. I presumed the stack to be
> thread-local, but failed to write it down.)

As noted above, I don't see any way for that to help. Feel free to set me
straight if I'm wrong.

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

From: Erhard Ploedereder
Sent: Monday, October 8, 2012  7:46 PM

> The infinite recursion:
   ...
> So I think this problem is unfixable. We could adopt one or more rules
> to minimize it, but it can't be eliminated.

Well, I do not believe that yet. What about the notion of (unchecked) inner
calls vs. (checked) outer calls of primitive ops, with the understanding that
calls in pre/post/invariants qualify as inner calls? It is easily decided
statically (because "inner" is a syntactic concept), enforces the invariant at
the interface to the outside world, but does not enforce it "internally", which
is how type invariants usually work, don't they?

Yes, Tuck said that this is not the present Ada model. But, with that model, you
really have to work hard to create the infinite recursion (via a call-out that
calls back in - the latter does NOT qualify as an inner call even if the
call-chain to it originated "inside").

Anyway, this is probably academic, since there is no support for changing the
model significantly, and the "modified-in"-aspect addresses most concerns. I
don't like it, but I am willing to live with it, since the creator of the type
has the necessary controls.

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

From: Randy Brukardt
Sent: Monday, October 8, 2012  8:34 PM

> > The infinite recursion:
>    ...
> > So I think this problem is unfixable. We could adopt one or more
> > rules to minimize it, but it can't be eliminated.
>
> Well, I do not believe that yet. What about the notion of
> (unchecked) inner calls vs. (checked) outer calls of primitive ops,
> with the understanding that calls in pre/post/invariants qualify as
> inner calls?
> It is easily decided statically (because "inner" is a syntactic
> concept), enforces the invariant at the interface to the outside
> world, but does not enforce it "internally", which is how type
> invariants usually work, don't they?

I don't believe that this is "easily" decided statically, and in extreme cases,
it isn't even known statically.

The problem here is that you are bringing the notions of visibility and scope
into this problem, and are going to have to do so in unintuitive ways.
Specifically, you are going to have to have some sort of rules defining what is
"inner" and what is "outer" in child packages. I'm sure consistent rules could
be found, but I much doubt that they would be obvious.

In addition, you've got cases (like composition of equality) where you don't
actually know whether the call is inner or outer (depending on what you mean by
inner and outer). If your implementation is mostly based on thunks for record
types (as ours is), you'd probably have to pass an "inner/outer" flag into every
thunk. Yuck.

Equality, in particular, is likely to be used a lot in invariant expressions,
and I can imagine how composition could come into play in such cases. I don't
think you'd actually fix anything unless the rule was quite complex.

> Yes, Tuck said that this is not the present Ada model. But, with that
> model, you really have to work hard to create the infinite recursion
> (via a call-out that calls back in - the latter does NOT qualify as an
> inner call even if the call-chain to it originated "inside").

In order for that to be the case, equality composition would have to be both
inner and outer. I suspect that would not be easy to explain. (Imagine a record
type containing an access type that designates the access type, and a
user-defined equality for the access type, all in a single package.)

> Anyway, this is probably academic, since there is no support for
> changing the model significantly, and the "modified-in"-aspect
> addresses most concerns. I don't like it, but I am willing to live
> with it, since the creator of the type has the necessary controls.

Well, I don't like such an aspect either, unless it is applied to the type
invariant (not subprograms). (Applying such an aspect to subprograms eliminates
most of the value of type invariants, which is to detect bugs that you've never
imagined [after all, if you imagined them, you probably eliminated them from the
design; it's the problems you didn't think of that bite so hard]. If they aren't
automatically checked, you'll never find the actual bugs.)

But if that's the case, the recursion problem still remains. That's why I prefer
almost any other solution that has been proposed (but especially the
"Do_not_check_invariants_on_in_parameters" aspect).

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

From: Robert Dewar
Sent: Monday, October 8, 2012  6:41 PM

> I had to modify the
> task attribute ACATS tests to allow rejection because some existing
> implementations only allowed a single task attribute.)

I consider an implementation that allows only a single task attribute to be
non-conforming from a practical point of view. Yes, formally it is allowed, but
it also allowed to raise Storage_Error on the execution of every ACATS C tests,
and no one would believe this is acceptable.

The ACATS tests should be making sure that compilers have no unreasonable
arbitrary limits on what they can accept, even though the RM in a formal sense
allows any limits on anything, and as I say, allows SE to be raised anywhere.

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

From: Randy Brukardt
Sent: Monday, October 8, 2012  8:17 PM

In this case, there is a specific rule (C.7.2(29)) allowing such an
implementation, so it could not be justified to require anything else in the
ACATS. This is not a general question of capacity, but rather a specific
permission given in the Standard.

In general, I agree with you, and I surely would not have made such a test
change without the explicit permission to restrict the number of attributes. We
could of course consider repealing or modifying C.7.2(29), but I think we'd need
more of a reason than "I consider an implementation that allows only a single
task attribute to be non-conforming from a practical point of view".

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

From: Robert Dewar
Sent: Monday, October 8, 2012  8:49 PM

> In this case, there is a specific rule (C.7.2(29)) allowing such an
> implementation, so it could not be justified to require anything else
> in the ACATS. This is not a general question of capacity, but rather a
> specific permission given in the Standard.

I still think it is unreasonable to intepret C.7.2(29) to allow arbitrary and
ludicrous restrictions. The idea of this clause is to acknowledge that in some
operating systems, there may be natural limits, but it is a distortion to allow
this. After all you could even argue "I fully implement this feature, but the
maximum number of task attributes is zero". This is of course nonsense. But a
maximum number of 1 is just as nonensical.

As I say, please remember the standard allows you to raise SE any time you feel
like it!

> In general, I agree with you, and I surely would not have made such a
> test change without the explicit permission to restrict the number of attributes.
> We could of course consider repealing or modifying C.7.2(29), but I
> think we'd need more of a reason than "I consider an implementation
> that allows only a single task attribute to be non-conforming from a
> practical point of view".

I don't remember this being discussed, but I may just be forgetting

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

From: Randy Brukardt
Sent: Monday, October 8, 2012  9:33 PM

> I don't remember this being discussed, but I may just be forgetting

Well, I just looked this up, and it happened much longer ago than I thought.
Indeed, it was one of the first test petitions I handled, in January of 1999.
I'm not surprised that you forgot about it. It was discussed on the FRT list,
including you and Tucker.

Here's the complete ruling:

This message conveys the ACAA ruling for the petition against for ACATS 2.1 test
programs CXC7002 and CXC7003.  This petition is accepted.

The petitioner states that the implementation permission C.7.2(29) allows an
implementation to raise Storage_Error when instantiated Ada.Task_Attributes in
these tests.

The ACAA has consulted its panel of experts on this issue. While the experts
agree that it is not desirable to allow implementations to essentially disable
this feature, there is no agreement on what the minimum requirements ought to
be. There is, however, agreement that more than one attribute should be
supported, and that attributes should be able to hold an access value or
similarly sized value.

Therefore, the ACAA has modified the test CXC7002 to insure that all attributes
tested are smaller than the size of an access value. The ACAA has modified test
CXC7003 to print a Not_Applicable result if an exception is raised by the
instantiation or first use of Set_Value for the Task_Attributes. The modified
test are available on the ACAA web site (www.ocsystems.com/~acats/), and will be
issued with the next Modified Tests List (2.1E).

---------

So I mis-remembered the "one attribute". CXC7002 actually requires two, of the
size of an access value. (Hardly different, IMHO.)

I think the problem really still comes down to: "there is no agreement on what
the minimum requirements ought to be". In the absence of that, it would be hard
to make any serious requirement in the ACATS or the RM.

P.S. The FRT thread is interesting reading. I summarized it thusly at the
time:
"Well, I haven't seen this much flip-flopping since my dad drained the goldfish
pond without removing the fish." ;-)

Essentially, we started with a number of people saying that the tests were
reasonable, and they shouldn't be modified (and a few others saying that
anything should be allowed). Then (after more input from the petitioner),
everyone flipped to a position of modify the tests to allow attributes to be
limited to access size.

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

From: Robert Dewar
Sent: Monday, October 8, 2012  9:43 PM

> I think the problem really still comes down to: "there is no agreement
> on what the minimum requirements ought to be". In the absence of that,
> it would be hard to make any serious requirement in the ACATS or the RM.

Well there is also no agreement on the size of subprograms that must be handled
or many other limits, but nevertheless the ACATS tests impose some reasonable
limits.

> Essentially, we started with a number of people saying that the tests
> were reasonable, and they shouldn't be modified (and a few others
> saying that anything should be allowed). Then (after more input from
> the petitioner), everyone flipped to a position of modify the tests to
> allow attributes to be limited to access size.

Allowing attributes to be limited to access size is not unreasonable, allowing
only two is bogus.

A better approach in the RM would be to completely remove this paragraph. Then
if an implementation has a GOOD reason for limiting the number or size, e.g. OS
limitations, it can argue for an exception under the general rule of not
requiring implementations to do unreasonable things.

Oh well water under the proverbial bridge, does the affected implementation
still exist? :-)

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

From: Randy Brukardt
Sent: Monday, October 8, 2012  10:03 PM

...
> Oh well water under the proverbial bridge, does the affected
> implementation still exist? :-)

The implementation exists (I've had occasional contact with that vendor, most
recently in July), but whether the specific target is still supported I have no
knowledge.

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

From: Bob Duff
Sent: Tuesday, October 9, 2012   9:06 AM

>... C.7.2(29)

is off topic for this thread, which is already too long for me to follow.  Could
we please stay focussed?  (I must admit that the side issue is indeed more
interesting!)

Randy wrote, quoting himself:

> "Well, I haven't seen this much flip-flopping since my dad drained the
> goldfish pond without removing the fish." ;-)

Better not run for Pres.  That's right up there with Romney's dog-on-car-roof
story.  ;-)

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

From: Bob Duff
Sent: Tuesday, October 9, 2012   9:07 AM

> The likelihood of any implementor doing *anything* with Text_IO is
> amazingly minimal! :-)

Yes, indeed.  The point of the Text_IO example is that people write code similar
to Text_IO, and it would be nice to have invariants working nicely for that sort
of code.  The GNAT front end is full of that sort of code:  we have "N: in
Node_Id" params all over, and then say "Set_Some_Field(N, ...);".  It works
because Node_Id is a pointer (represented as an index into a table).

Here's an idea:  An attribute that takes away the invariant on a private type.
It denotes a subtype of the private type that has no invariant.  Then you can
declare some parameters with the private type, and they get checked (including
'in'). For things you call from the invariant itself, you declare the parameters
to be of the without-invariant subtype.  This would give the per-subprogram
control that Tuck wants.

Now we already have something like that for scalars:  T'Base is the same as T,
but with all the constraints and predicates removed. So I'm suggesting we could
allow 'Base on all types.  For access types, T'Base would remove the null
exclusions and predicates. For composite types, T'Base would remove the
predicates and invariants. (I think you don't want to allow removal of
discriminant or index constraints, because I think it would introduce the
anomalies that caused us to disallow Composite'Base back in Ada 9X.  I don't
remember the details.)

> You left out the simplest solution at all: have an aspect to declare
> that a routine is used in a type invariant. In which case no invariant
> checks are done for the routine; otherwise, the checks are done as
> specified in the language.

This is very similar to what I'm proposing.  But you don't want to say "this is
used in an invariant".  You want to say "don't check the invariant on this".

> That's more flexible than just limiting to expression functions, and
> has far fewer holes than never checking invariants on IN parameters
> (and would never cause a hole unintentionally, as the expression function rule might).

Right, and I like the idea that invariants are checked in "in"s by default, and
you can specify otherwise.

> No one seems to have seriously considered this idea other than me;
> that could be because everyone hates it, but no one has said that or
> tried to explain why. More likely it's because no one noticed the idea.

I seriously considered it, and I think it's a good approach -- I just hadn't
gotten around to replying (this thread is way too long!).

> I believe whatever solution we produce should prevent infinite
> recursion at compile-time due to type-invariant checks, in all but the
> most obscure cases.  I don't think the programmer should have to think
> about/worry about this problem at all, and shouldn't have to create wrappers, etc.
> to avoid infinite recursion.  The programmer should be able to write
> the most natural and appropriate type invariant, and it should work as
> expected.

I disagree with that.  What is "expected" is that the invariant is True. If
certain cases are exempted from invariant checks, they should be explicit, as in
my 'Base idea.  (Yes, I know there are all sorts of other loopholes.)

As to infinite recursion, it seems similar to having a Pre on function F call
function F.  So don't do that.  And get your friendly compiler writer to warn in
some cases.

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

From: Tucker Taft
Sent: Tuesday, October 9, 2012  9:25 AM

>> ... I believe whatever solution we produce should prevent infinite
>> recursion at compile-time due to type-invariant checks, in all but
>> the most obscure cases.  I don't think the programmer should have to
>> think about/worry about this problem at all, and shouldn't have to create wrappers, etc.
>> to avoid infinite recursion.  The programmer should be able to write
>> the most natural and appropriate type invariant, and it should work
>> as expected.
>
> I disagree with that.  What is "expected" is that the invariant is True.
> If certain cases are exempted from invariant checks, they should be
> explicit, as in my 'Base idea.  (Yes, I know there are all sorts of
> other loopholes.)
>
> As to infinite recursion, it seems similar to having a Pre on function
> F call function F.  So don't do that.  And get your friendly compiler
> writer to warn in some cases.

But a Pre on F that calls F is very unlikely.  On the other hand, a
Type_Invariant that calls a public function is very likely.

How about we *require* that the Type_Invariant expression not involve a direct
call on a function to which the Type_Invariant applies?  I.e., it is a mandatory
check, but only one level.  This will at least make the average programmer aware
of the issue, and then we can debate how best to make it possible to deactivate
the Type_Invariant on a particular subprogram.  You are suggesting using a
different type mark, Randy is suggesting a new aspect to suppress it, I was
suggesting that you only get it if you ask for it on IN parameters, etc.  If we
can all agree that the compiler *must* detect a direct call in a Type_Invariant
aspect on a function to which a Type_Invariant applies, then (I think ;-) I am
happy...

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

From: Robert Dewar
Sent: Tuesday, October 9, 2012  9:43 AM

> Here's an idea:  An attribute that takes away the invariant on a
> private type.  It denotes a subtype of the private type that has no
> invariant.  Then you can declare some parameters with the private
> type, and they get checked (including 'in').
> For things you call from the invariant itself, you declare the
> parameters to be of the without-invariant subtype.  This would give
> the per-subprogram control that Tuck wants.

interesting idea!

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

From: Bob Duff
Sent: Tuesday, October 9, 2012  12:17 PM

> How about we *require* that the Type_Invariant expression not involve
> a direct call on a function to which the Type_Invariant applies?

OK.

>...  I.e., it
> is a mandatory check, but only one level.  This will at least make the
>average programmer aware of the issue, and then we can debate how best
>to make it possible to deactivate the Type_Invariant on a particular
>subprogram.  You are suggesting using a different type mark, Randy is
>suggesting a new aspect to suppress it, I was suggesting that you only
>get it if you ask for it on IN parameters, etc.

Right.  I prefer my 'Base idea to the other two, because it seems simple, and it
seems generally useful.  In fact, I use it all the time on scalar types with
predicates.

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

From: Randy Brukardt
Sent: Tuesday, October 9, 2012  3:27 PM

...
> > I disagree with that.  What is "expected" is that the invariant is True.
> > If certain cases are exempted from invariant checks, they should be
> > explicit, as in my 'Base idea.  (Yes, I know there are all sorts of
> > other loopholes.)
> >
> > As to infinite recursion, it seems similar to having a Pre on
> > function F call function F.  So don't do that.  And get your
> > friendly compiler writer to warn in some cases.
>
> But a Pre on F that calls F is very unlikely.  On the other hand, a
> Type_Invariant that calls a public function is very likely.

Almost required, in fact, for Type_Invariant'Class, which has to be public.

> How about we *require* that the Type_Invariant expression not involve
> a direct call on a function to which the Type_Invariant applies?
> I.e., it is a mandatory check, but only one level.  This will at least
> make the average programmer aware of the issue, and then we can debate
> how best to make it possible to deactivate the Type_Invariant on a
> particular subprogram.  You are suggesting using a different type
> mark, Randy is suggesting a new aspect to suppress it, I was
> suggesting that you only get it if you ask for it on IN parameters,
> etc.  If we can all agree that the compiler *must* detect a direct
> call in a Type_Invariant aspect on a function to which a
> Type_Invariant applies, then (I think ;-) I am happy...

I can agree that making this a legality rule is a good idea, so long as it can
checked sanely (meaning that whatever trigger we use, it has to be visible on
the specification of the routine(s) in question).

I'm still partial to the
   Do_Not_Check_Type_Invariant
aspect. I'm a bit dubious that Bob's extra subtype adds much clarity:
    subtype Unchecked_File_Type is File_Type
        with No_Invariant_Check;
but I certainly can live with it.

I'm definitely against the idea of getting checking only if you ask -- that's
not usually how Ada works. You usually get checking unless you take some action
to stop it; that's the way to catch the most errors. I don't see any good reason
for this case to be different.

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

From: Tucker Taft
Sent: Thursday, December 6, 2012  9:26 PM

Following up on my bounded-error idea for IN parameters --

Instead of a bounded error, simply make it an implementation permission to
perform an invariant check on an IN parameter, so long as the call does not
originate during an evaluation of the same invariant.  That is, it is
required on IN OUT and OUT parameters, but permitted on IN parameter when
implementation can be sure this won't result in recursion.

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

From: Yannick Moy
Sent: Friday, December 7, 2012  3:11 AM

This is a great idea, because it also gives a nice path forward with proving
statically invariants. The issue with the original wording on invariants is
that, since it does not say that invariants hold on entry for IN and IN OUT
parameters, you cannot do modular proofs based on those. Which means in fact
that you have to add these constraints to make modular proof feasible. If the
RM states what you just said, the constraint is already in place, even if not
checked dynamically!

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

Questions? Ask the ACAA Technical Agent