!standard 6.1.1(0)                                11-07-24    AI05-0254-1/03
!standard 3.9.2(20.2/2)
!reference AI05-0247-1
!class Amendment 11-06-16
!status Amendment 2012 11-07-22
!status ARG Approved 9-0-3  11-06-25
!status work item 11-06-16
!status received 11-06-05
!priority High
!difficulty Hard
!subject Do we REALLY have contracts right?
!summary

Improve the wording proposed in AI05-0247-1.

!question

The fixes made in AI05-0247-1 have some ARG members uncomfortable.
Should we reconsider? (Only the wording.)

!proposal

(See wording.)

!wording

Modify 3.9.4(20.4/3):

otherwise, the action is the same as the action for the corresponding operation of
the parent type or progenitor type from which the operation was inherited
{(except that additional class-wide postconditions may apply -- see 6.1.1)}.
If there is more than one such corresponding operation, the action is that for
the operation that is not a null procedure, if any; otherwise, the action is
that of an arbitrary one of the operations.

Modify 6.1.1(3/3):

This aspect specifies a class-wide precondition for a callable entity and its
descendants; it shall be specified by an expression, called a class-wide
precondition expression. If not specified for an entity, {then if no other
class-wide precondition applies to the entity,} the class-wide precondition
expression for the entity is the enumeration literal True.

Add a new AARM Ramification after 6.1.1(3/3):

If other class-wide preconditions apply to the entity and no class-wide
precondition is specified, no class-wide precondition is defined for the entity;
of course, the class-wide preconditions (of ancestors) that apply are still going
to be checked. We need subprograms that don't have ancestors and don't specify a
class-wide precondition to have a class-wide precondition of True, so that adding
such a precondition to a descendant has no effect (necessary as a dispatching call
through the root routine would not check any class-wide precondition).

Replace 6.1.1(10-12/3) with:

If a type T has an implicitly declared subprogram P inherited from a parent type T1
and a homograph (see 8.3) of P from a progenitor type T2, and

* the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and

* the class-wide precondition expression True does not apply to P1 (implicitly or
  explicitly); and

* there is a class-wide precondition expression that applies to the corresponding primitive
  subprogram P2 of T2 that does not fully conform to any class-wide precondition that applies to P1,

then:

* If the type T is abstract the implicitly declared subprogram P is *abstract*.

* Otherwise, the subprogram P *requires overriding* and shall be overridden with a
  nonabstract subprogram.


Modify 6.1.1(23/3):

The {checks are performed in an arbitrary order}[order of performing the checks
is not specified], and if any of the
class-wide precondition expressions evaluate to True, it is not specified
whether the other class-wide precondition expressions are evaluated. {The
precondition checks and any check for elaboration of the subprogram body are
performed in an arbitrary order}[It is not
specified whether any check for elaboration of the subprogram body is
performed before or after the precondition checks]. It is not specified whether
in a call on a protected operation, the checks are performed before or after
starting the protected action. For a task or protected entry call, the checks
are performed prior to checking whether the entry is open.

Modify 6.1.1(24/3):

If the assertion policy in effect at the point of a subprogram or entry
declaration is Check, then upon successful return from a call of the
subprogram or entry, prior to copying back any by-copy *in out* or *out*
parameters, the postcondition check is performed. This consists of the
evaluation of the specific and class-wide postcondition expressions that apply
to the subprogram or entry. If any of the postcondition expressions
evaluate to False, then Ada.Assertions.Assertion_Error is raised.
The {postcondition expressions are evaluated in an arbitrary order}[order of
performing the checks is not specified], and if any
postcondition expression evaluates to False, it is not specified whether any other
postcondition expressions are evaluated. {The postcondition check and constraint checks
associated with copying back @b<in out> or @b<out> parameters are performed in an
arbitrary order}[It is not specified whether any constraint checks associated with
copying back in out or out parameters are performed before or after the postcondition
checks].

Replace 6.1.1(26/3) with:

For any subprogram or entry call (including dispatching calls), the checks
that are performed that verify specific precondition expressions and specific
and class-wide postcondition expressions are determined by those for the subprogram
or entry actually invoked. Note that the class-wide postcondition expressions
verified by the postcondition check that is part of a call on a primitive
of type T includes all class-wide postcondition expressions originating
in any progenitor of T [Redundant: , even if the primitive called
is inherited from a type T1 and some of the postcondition expressions do
not apply to the corresponding primitive of T1].


Replace 6.1.1(27/3) with:

The class-wide precondition check for a call to a subprogram or entry consists
solely of checking the class-wide precondition expressions that apply to the denoted
callable entity (not necessarily the one that is invoked).

For a call via an access-to-subprogram value, all precondition and postcondition checks
performed are determined by the subprogram or entry denoted by the prefix of the Access
attribute reference that produced the value.

!discussion

The broad changes made in AI05-0247-1 are necessary to preserve LSP, to
allow programmers and compilers to trust contracts, and to allow static
analyzability of dispatching calls. There really aren't any other solutions
that have all of these properties.

Specifically, the way class-wide preconditions and postconditions are
combined is required by LSP. Separating specific preconditions into a
separate check eliminates counter-intuitive semantics without (directly)
violating LSP.

Having the class-wide precondition check on a dispatching call check the
preconditions known to the call rather than those known to the body allows
static analysis of the contracts of such calls, has no effect on correctness
(as the body must have a weaker precondition), and makes more obvious to the
programmer of such a call what the class-wide precondition is (so they can
meet it).

But most of the effort of AI05-0247-1 was spent on the details of inherited
routines that have additional contracts added (via interfaces).

It eventually was decided to make such preconditions illegal (the routine
requires overriding), and require the postconditions to be evaluated as-if
there is an overriding body. The precondition case is a problem as it either
requires violating LSP or calling a routine with the preconditions it knows
about False -- neither seem like a good idea.

The details of the wording to accomplish that were very hard to arrive at,
and needed more polishing.

However, these cases are not at all important to the success or failure of
Ada 2012. Indeed, they are just short of a pathology; still, we need to have
an answer for them.

In particular, the case of inheriting a routine from a base type that is also
defined by an interface that is being added to a derived type is very unlikely
to occur in practice -- and if it does occur, the programmer has a major design
problem on their hands that will outweigh any rules we do or don't adopt.

Most of the time, when an interface is added to a derived type, the operations
to implement that interface are added at the same time. They're not inherited
from the parent type. Indeed, it doesn't make sense for them to be defined
on the parent type, because it doesn't make sense to have the operations
separately from the interface. For instance, if an interface implements
persistence, it makes little sense to add that to a type that already supports
persistence (it makes much more sense to add the interface to the base type
in that case).

Moreover, when the operations do already exist, it is unlikely that they
have the appropriate profile and contracts to implement the interface. So
again the interface will be implemented with new operations.

Of course, the programmer could be unlucky and have a collision of unrelated
routines. In that case, something will have to be renamed, and we surely will
not want the inherited routine to come through unchanged (it will be wrong for
one use or the other).

It is very unlikely that none of these things will happen, and everything is
perfect -- and that is the only case where the rules that we adopt for collisions
of preconditions and postconditions matter.

!corrigendum 3.9.2(20.2/2)

@drepl
Force a conflict; the real text is found in the conflict file.
@dby
Nothing interesting.

!corrigendum 6.1.1(0)

@dinsc

Force a conflict; the real text is found in the conflict file.

!ACATS test

An ACATS B-Test to check the newly revised legality rules should be
constructed.

ACATS C-Tests should be constructed to ensure that preconditions and
postconditions are evaluated as specified in this wording (and AI05-0247-1).
Specifically:

 * Check that the specific precondition and the specific
   postcondition of an inherited routine are evaluated (even though an
   overridden routine would not have those specific pre and post conditions).

 * Check that the class-wide preconditions of any (new) progenitors are
   evaluated for a statically-bound call to an inherited routine.

 * Check that the class-wide postconditions of any (new) progenitors are
   evaluated for a statically-bound, dispatching, and access-to-subprogram
   call to an inherited routine (of a type that doesn't have those
   progenitors).

 * Check that the class-wide preconditions of a dispatching call are those
   of the nominal call. In particular, check the case where the dispatching
   call is for type A, and the class-wide precondition is PA; the actual object
   is type B derived from A with progenitor I, and class-wide precondition of
   IA is PB, PB is True for the actual object and PA is False. In this case,
   the precondition should fail on the dispatching call (while an incorrect
   implementation using the precondition of the invoked call would succeed).

!ASIS

Any ASIS impact should be have been handled as part of the original
precondition/postcondition AI (AI05-0145-2) - this AI only affects dynamic
semantics and legality rules and neither of those are concerns of ASIS.

!appendix

From: Tucker Taft
Sent: Sunday, June  5, 2011  8:59 AM

I realize the hope was that all AIs would be settled by the June ARG meeting,
but I believe that AI-247 needs some face-to-face time.  Because it is about
something which we see as the cornerstone of Ada 2012 (contracts), I don't think
we want to allow it to go into the standard without an informed consensus that
it is the "right" answer.

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

From: Randy Brukardt
Sent: Monday, June 6, 2011  2:02 PM

> I realize the hope was that all AIs would be settled by the June ARG
> meeting, but I believe that AI-247 needs some face-to-face time.
> Because it is about something which we see as the cornerstone of Ada
> 2012 (contracts), I don't think we want to allow it to go into the
> standard without an informed consensus that it is the "right" answer.

Well, I don't agree with the notion that we would somehow change the major
thrust of the AI, given that there really isn't any other solutions that would:
   (A) Preserve LSP in all language-defined situations; and
   (B) Allow subprograms to "trust" their preconditions and allow callers to
       "trust" their postconditions. ("trust" is in quotes because contract
       expressions that have or depend on side-effects can never be trusted, but
       the majority of contracts aren't in this category).

(A) is necessary for a variety of purposes, including allowing callers to know
the preconditions of called dispatching routines (necessary both for
understanding and for proof purposes). (B) is necessary so that these truly act
like contracts (and not random assertions), and programmers (and tools) can
reason about them.

I've always presumed that everyone agrees with (A) and (B) -- if not, we have
truly serious problems with the entire contract concept.

If so, the broad solution outlined in AI05-0247-1 is the only option. (Well,
there is one other option -- abandon all attempt to support contracts on OOP --
not acceptable IMHO).

We were bogged down by wording issues mostly having to do with specific unlikely
corner cases. These warrant some discussion, but it does not rise to the level
of reopening the AI.

If we *really* want a "informed consensus" on this issues, someone will need to
prepare a tutorial on these issues, as I suspect that many of the ARG members
are lost (especially when it comes to the details). That's going to take most of
the meeting by itself...

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

From: Tucker Taft
Sent: Saturday, June 25, 2011  3:43 AM

6.1.1 paras 10-12:

   If a type T inherits homographs from a parent type T1 and a progenitor
   type T2, and

      * the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and
      * a class-wide precondition applies to the corresponding primitive subprogram P2 of
        T2 that does not fully conform to any class-wide precondition that applies to P1,

   then:

     * If the type is abstract the implicitly declared subprogram P is *abstract*.

     * Otherwise, the subprogram P *requires overriding* and shall be overridden
       with a nonabstract subprogram.

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

From: Tucker Taft
Sent: Saturday, June 25, 2011  4:00 AM

6.1.1 paras 10-12 again:

   If a type T inherits homographs from a parent type T1 and a progenitor
   type T2, and

      * the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and
      * the class-wide precondition True does not apply to P1; and
      * a class-wide precondition applies to the corresponding primitive subprogram P2 of
        T2 that does not fully conform to any class-wide precondition that applies to P1,

   then:

     * If the type T is abstract the implicitly declared subprogram P is *abstract*.

     * Otherwise, the subprogram P *requires overriding* and shall be overridden
       with a nonabstract subprogram.

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

From: Tucker Taft
Sent: Saturday, June 25, 2011  4:04 AM

6.1.1 paras 10-12 (one more time):

   If a type T has an implicitly declared subprogram P inherited
   from a parent type T1 and a homograph of P from a
   progenitor type T2, and

      * the corresponding primitive subprogram P1 of type T1 is neither null nor
	abstract; and
      * the class-wide precondition True does not apply to P1; and
      * a class-wide precondition applies to the corresponding primitive
	subprogram P2 of T2 that does not fully conform to any class-wide
	precondition that applies to P1,

   then:

     * If the type T is abstract the implicitly declared subprogram P is
       *abstract*.

     * Otherwise, the subprogram P *requires overriding* and shall be overridden
       with a nonabstract subprogram.

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

From: Tucker Taft
Sent: Saturday, June 25, 2011  4:08 AM

6.1.1 (26) and (27):

   For any subprogram or entry call (including dispatching calls), the
   specific precondition and postcondition checks that are performed are
   determined by those of the subprogram or entry actually invoked.  The
   class-wide postcondition check that is performed on a call of a
   primitive of type T includes class-wide postconditions inherited from
   progenitors of T [Redundant: , even if the primitive is inherited from
   a type T1 and these postconditions do not apply to the corresponding
   primitive of T1].

We now take you to 3.9.2(20.4):

   otherwise, the action is the same as the action for the corresponding
   operation of the parent type or progenitor type from which the operation was
   inherited {(except that additional class-wide postconditions may apply -- see
   6.1.1)}. If there is more than one such corresponding operation, the action
   is that for the operation that is not a null procedure, if any; otherwise,
   the action is that of an arbitrary one of the operations.

Back to 6.1.6(27):

   For a call via an access-to-subprogram value, the class-wide precondition
   check performed is determined by the subprogram or entry denoted by the
   prefix of the Access attribute reference that produced the value. In
   contrast, the class-wide precondition check for other calls to a subprogram
   or entry consists solely of checking the class-wide preconditions that apply
   to the denoted entity (not necessarily the one that is invoked).

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

From: Tucker Taft
Sent: Saturday, June 25, 2011  4:27 AM

6.1.1(27) again (now 2 paragraphs):

   The class-wide precondition check for a call to a subprogram
   or entry consists solely of checking the class-wide preconditions that apply
   to the denoted callable entity (not necessarily the one that is invoked).

   For a call via an access-to-subprogram value, all precondition and
   postcondition checks performed are determined by the subprogram or entry
   denoted by the prefix of the Access attribute reference that produced the
   value.

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

From: Randy Brukardt
Sent: Friday, July 22, 2011  10:41 PM

I had a note to index 6.1.1(24) as "unspecified". But I wonder if the wording is
completely right. This paragraph says:

If the assertion policy in effect at the point of a subprogram or entry
declaration is Check, then upon successful return from a call of the subprogram
or entry, prior to copying back any by-copy in out or out parameters, the
postcondition check is performed. This consists of the evaluation of the
specific and class-wide postcondition expressions that apply to the subprogram
or entry. If any of the postcondition expressions evaluate to False, then
Ada.Assertions.Assertion_Error is raised. The order of performing the checks is
not specified, and if any postcondition expression evaluates to False, it is not
specified whether any other postcondition expressions are evaluated. It is not
specified whether any constraint checks associated with copying back in out or
out parameters are performed before or after the postcondition checks.

"The order of performing the checks is not specified" is not the usual way of
saying this. Usually we would say "The checks are performed in an arbitrary
order". That's important as "arbitrary order" has a definition (1.1.4(18)) and
is used in other rules.

However, I have to wonder if there was any intent to avoid 1.1.4(18) with this
wording. I would guess not (Tucker is not usually that clever without
documenting that cleverness; and I know that my earlier rewrite of this
paragraph did not change this aspect). In particular, 6.4.1(6.17/3) does not
apply to pre/postcondition checks whether or not "arbitrary order" is used (the
precondition and postcondition expressions are not "direct constituents" of the
subprogram call that caused them to be checked).

So I would suggest that the last two sentences here be replaced by:

The checks are performed in an arbitrary order, and if any postcondition
expression evaluates to False, it is not specified whether any other
postcondition expressions are evaluated. The postcondition checks and constraint
checks associated with copying back in out or out parameters are performed in an
arbitrary order.

Any objections???

P.S. An unrelated aside: as 6.4.1(6.17/3) might apply to every place in the
standard that talks about "arbitrary order", I indexed all such places as
"arbitrary order, allowed", and added an AARM note after 6.4.1(6.17/3) to
suggest using the index to find those places, while noting that not all will
apply (for instance, ones solely associated with checks or finalization won't
trigger this rule).

P.P.S. I suspect a similar rewording will be needed somewhere in the
type_invariant section 7.3.2(0) -- I'll worry about that when I get to it in the
next few days.

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

From: Jean-Pierre Rosen
Sent: Saturday, July 23, 2011  12:38 AM

Side question:
> If the assertion policy in effect at the point of a subprogram or
> entry
...

"subprogram or entry" is used several times in this paragraph. Why not use
"callable entity", which is defined (6(2)) to mean exactly that?

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

From: Randy Brukardt
Sent: Saturday, July 23, 2011  2:07 AM

> Side question:
> > If the assertion policy in effect at the point of a subprogram or
> > entry
> ...
>
> "subprogram or entry" is used several times in this paragraph. Why not
> use "callable entity", which is defined
> (6(2)) to mean exactly that?

I didn't write this, but I suspect that it's because this wording talks about
calls quite a bit, and "call of the callable entity" is not particularly
readable.

And I don't find "callable entity" much more readable than "subprogram or entry"
(assuming there is no problem with other conjunctions, which doesn't seem to
happen in this paragraph). In my own writing, I'd almost always use "subprogram
or entry" (or just forget entry altogether, can't do that in the standard of
course). A savings of 4 characters per use doesn't make up for using "bigger"
words and an unfamiliar term.

I did a quick and sloppy check of the AARM, and found 43 occurrences of
"callable entity" (several in index entries) and 29 occurrences of "subprogram
or entry". I didn't make any effort to see which is used more in the normative
text, but it seems that each is acceptable.

I don't feel strongly, of course, so if there is a groundswell, I'll change it
(and should do so in all 29 places, I think).

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

From: Tucker Taft
Sent: Saturday, July 23, 2011  8:16 AM

No objection.  Or as Bob might say, "shrug."

> I had a note to index 6.1.1(24) as "unspecified". But I wonder if the
> wording is completely right. This paragraph says:
> ...
> "The order of performing the checks is not specified" is not the usual
> way of saying this. Usually we would say "The checks are performed in
> an arbitrary order". That's important as "arbitrary order" has a
> definition
> (1.1.4(18)) and is used in other rules.
> ...
> Any objections???

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

From: Bob Duff
Sent: Saturday, July 23, 2011  8:51 AM

No objection from me, either.  And no shrug, really
-- although this is hardly important, Randy's proposed change is exactly right.

As to "callable entity": shrug.  But Randy's worry about "call of the callable
entity" is unwarranted -- just say "call of the entity"
or "call of that entity", and it's clear you're talking about the callable one
just mentioned.

Or just leave it alone.

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

From: Tucker Taft
Sent: Saturday, July 23, 2011  9:03 AM

> No objection from me, either.  And no shrug, really
> -- although this is hardly important, Randy's proposed change is
> exactly right.

Oh dear.  Is this something like "putting words in your mouth"?
Perhaps "putting a shrug in your shoulders"?  ;-)

I agree, Randy's proposed change is the right one.

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

From: Randy Brukardt
Sent: Sunday, July 24, 2011  7:40 PM

> As to "callable entity": shrug.  But Randy's worry about "call of the
> callable entity" is unwarranted -- just say "call of the entity"
> or "call of that entity", and it's clear you're talking about the
> callable one just mentioned.
>
> Or just leave it alone.

I'm definitely in "leave it alone" mode. I don't think your suggestion works
(everywhere). There is at least one paragraph that starts "For any subprogram
or entry call (including dispatching calls), ...". Changing this to "For any
callable entity call (including dispatching calls), ..." looks silly, and
replacing it by "For any call to an entity (including dispatching calls)..."
seems to me at least to have left out too much information (it leaves one
wondering what sort of calls are involved).

It's so late in the game that messing with correct wording doesn't seem
worthwhile, especially when there is plenty of wording that is not quite
right...

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

From: Randy Brukardt
Sent: Saturday, July 23, 2011  12:40 AM

I'm worried about the fact that class-wide preconditions have a default value of
True if not specified.

That's absolutely necessary for the conformance rules of 6.1.1(10-13/3) to work.
For instance, the revised wording from the recent meeting includes the following
bullet:

* there is a class-wide precondition that applies to the corresponding primitive
  subprogram P2 of T2 that does not fully conform to any class-wide precondition
  that applies to P1,

We need the class-wide precondition to be True by default to catch cases like
the following:

    package P1 is
       type T1 is tagged private;
       function Is_OK (Obj : T1) return Boolean;
       procedure P (Obj : in out T1)
          with Precondition'Class => Is_OK (Obj);
    end P1;

    package P2 is
       type T2 is interface;
       procedure P (Obj : in out T2); -- No class-wide precondition specified here.
    end P2;

    with P1, P2;
    package P3 is
       type T is new P1.T1 and P2.T2 with ...;
       -- Inherits P1.P here.
    end P3;

This violates the rule above as True (the class-wide precondition of P2.P) does
not conform to any class-wide precondition of P1.P (the only one is Is_OK
(Obj)). If instead P2.P has no class-wide precondition, we'd need a more complex
rule to detect this case (and we'd also need a more complex second bullet to
except any subprogram that has any class-wide precondition of True).

Perhaps an even more important reason that we need True to be the default is so
that every tagged primitive has at least one class-wide precondition. If a
routine like P2.P had no class-wide precondition, it would be possible to add
one later for a descendant, which by definition would be stronger and would
violate LSP.

Also note that class-wide preconditions are not inherited in any way; checking a
preconditions involves checking the class-wide preconditions of yourself and of
all ancestors. So each subprogram has a single, unique class-wide precondition.

However, this does not work in the common case that all we want for an extension
is the same precondition as it's parent:

    with P1;
    package P3 is
       type T3 is new P1.T1 with private;
       overriding
       procedure P (Obj : in out T2);
    end P2;

Here the language says that the class-wide precondition of P3.P is True. This is
almost certainly not what we want (we probably just want to use the parent's
class-wide precondition). True would of course eliminate the precondition of the
parent from consideration. What we really want is for this routine to have no
class-wide precondition of it's own.

Note that none of the other contracts have this problem (extra True class-wide
postconditions have no effect, and specific ones aren't inherited anyway).

One solution would be to not have a default value from class-wide preconditions,
but then the wording of 6.1.1(10-13/3) will have to be totally redone, and other
wording would also have to be changed to avoid problems with later adding of
preconditions to descendants.

A better (maybe?) solution would be for the value of True to be the default if
and only if no other class-wide precondition "applies" to the subprogram; if any
other class-wide precondition applies, then there is no class-wide precondition
directly for this entity (of course, the class-wide preconditions that come from
ancestors still apply).

This would require wording like (6.1.1(3/3)):

This aspect specifies a class-wide precondition for a callable entity and its
descendants; it shall be specified by an expression, called a class-wide
precondition expression. If not specified for an entity, then if no other
class-wide precondition applies to the entity, the class-wide precondition
expression for the entity is the enumeration literal True.

AARM Ramification:
If other class-wide preconditions apply to the entity and no class-wide
precondition is specified, no class-wide precondition is defined for the entity;
of course, the class-wide preconditions (of ancestors) that apply are still
going to be checked. We need routines that don't have ancestors and don't
specify a class-wide precondition to have a class-wide precondition of True, so
that adding such a precondition to a descendant has no effect (necessary as a
dispatching call through the root routine would not check any class-wide
precondition).

[I think I prefer to not say anything normative about the unspecified/"applies"
case; the entire explanation of the Ramification is necessary to avoid
confusion, and that is just too much verbiage.]

Can this be done better??

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

From: Tucker Taft
Sent: Saturday, July 23, 2011  8:22 AM

Your proposed wording seems reasonable to me.

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

From: Bob Duff
Sent: Saturday, July 23, 2011  4:29 PM

> This aspect specifies a class-wide precondition for a callable entity
> and its descendants; it shall be specified by an expression, called a
> class-wide precondition expression. If not specified for an entity,
> then if no other class-wide precondition applies to the entity, the
> class-wide precondition expression for the entity is the enumeration literal True.

I suggest leaving out "enumeration literal".  It's not really a piece of syntax
that gets resolved (e.g. if there's some other True lying around we don't use
that).  It's the True of boolean that live in Standard, and just saying "True"
seems clear enough.

Otherwise, I agree with the above wording.

> AARM Ramification:
> If other class-wide preconditions apply to the entity and no
> class-wide precondition is specified, no class-wide precondition is
> defined for the entity; of course, the class-wide preconditions (of
> ancestors) that apply are still going to be checked. We need routines
> that

"routines" --> "subprograms"?

> don't have ancestors and don't specify a class-wide precondition to
> have a class-wide precondition of True, so that adding such a
> precondition to a descendant has no effect (necessary as a dispatching
> call through the root routine would not check any class-wide precondition).

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

From: Randy Brukardt
Sent: Sunday, July 24, 2011  7:33 PM

> I suggest leaving out "enumeration literal".  It's not really a piece
> of syntax that gets resolved (e.g. if there's some other True lying
> around we don't use that).  It's the True of boolean that live in
> Standard, and just saying "True" seems clear enough.

I don't agree, as this is subject to full conformance in following Legality
Rules and being clear that we're not talking about the value True but rather a
specific expression True is important. (Full conformance depends on the specific
declaration involved.) Indeed, I worry that this is still too sloppy and we
really ought to say "enumeration literal True declared in package Standard (see
A.1)". Probably a To Be Honest would be good enough for that.

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

From: Randy Brukardt
Sent: Saturday, July 23, 2011  1:53 AM

The wording approved at the meeting for 6.1.1(26/3) says:

For any subprogram or entry call (including dispatching calls), the specific
precondition and postcondition checks that are performed are determined by those
of the subprogram or entry actually invoked. The class-wide postcondition check
that is performed on a call of a primitive of type T includes class-wide
postconditions inherited from progenitors of T [Redundant: , even if the
primitive is inherited from a type T1 and these postconditions do not apply to
the corresponding primitive of T1].

The major problem here is that there is no such thing as a "specific
postcondition check" or a "class-wide postcondition check". There are specific
and class-wide postcondition *expressions*, but there is just a single
postcondition check that covers everything (see 6.1.1(24)).

This was the definition that Tucker had originally given the check, and (unlike
the precondition cases), there was no semantic reason to split it up (they all
work the same way, raise an exception if False). So it remains a single check.
The second sentence here seems to be structured to recognize this reality (it
seems to indicate that there is only a single class-wide postcondition check,
which is bizarre as there never was any such model).

We could fix this by defining these as separate checks, but that would explode
6.1.1(24) from one paragraph into four (if the precondition wording is any
guide.

Alternatively, we could return the wording somewhat closer to its original form
(but note this is the wording that Erhard found confusing - I added a
parenthetical remark to clarify):

  For any subprogram or entry call (including dispatching calls), the specific
  precondition check and the postcondition check [Redundant: (which checks both
  specific and class-wide postcondition expressions, if any)] that are performed
  are determined by those of the subprogram or entry actually invoked. The
  postcondition check that is performed on a call of a primitive of type T
  includes class-wide postcondition expressions inherited from progenitors of T
  [Redundant: , even if the primitive is inherited from a type T1 and these
  postconditions do not apply to the corresponding primitive of T1].

A second (minor) problem is that class-wide postcondition expressions are not
"inherited"; they "apply", so the phrase "includes class-wide postconditions
inherited from progenitors of T" is nonsense in normative text. (And "class-wide
postconditions" is a term that is not defined at all). We could say something
like "includes class-wide postconditions expressions that apply solely because
they are defined for primitives of progenitors of T", but that seems pretty
wordy. Still, I don't have a better idea. That gives:

  For any subprogram or entry call (including dispatching calls), the specific
  precondition check and the postcondition check [Redundant: (which checks both
  specific and class-wide postcondition expressions, if any)] that are performed
  are determined by those of the subprogram or entry actually invoked. The
  postcondition check that is performed on a call of a primitive of type T
  includes class-wide postcondition expressions that apply solely because they
  are defined for primitives of progenitors of T [Redundant: , even if the
  primitive is inherited from a type T1 and these postconditions do not apply to
  the corresponding primitive of T1].

Any improvements will be appreciated.

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

From: Tucker Taft
Sent: Saturday, July 23, 2011  8:22 AM

> Alternatively, we could return the wording somewhat closer to its
> original form (but note this is the wording that Erhard found
> confusing - I added a parenthetical remark to clarify):
>
>    For any subprogram or entry call (including dispatching calls), the specific
>    precondition check and the postcondition check [Redundant: (which checks both specific
>    and class-wide postcondition expressions, if any)] that are performed are determined by
>    those of the subprogram or entry actually invoked. The postcondition
>    check that is performed on a call of a primitive of type T includes class-wide
>    postcondition expressions inherited from progenitors of T [Redundant: , even if the
>    primitive is inherited from a type T1 and these postconditions do not apply to the
>    corresponding primitive of T1].


I would prefer:

    For any subprogram or entry call (including dispatching calls), the checks
    that are performed for specific precondition expressions and all
    postcondition expressions are determined by those of the subprogram
    or entry actually invoked.  The postcondition check that is performed
    on a call of a primitive of type T verifies class-wide postcondition
    expressions inherited from progenitors of T ...

This finesses the whole issue of whether it is considered one check or two,
since the plural "checks" is correct either way.  It also emphasizes "all"
instead of simply allowing it to be implicit in the use of the unqualified term
"postcondition check."  It also avoids the notion that an expression is
"included" in a check, since it is really the evaluation of the expression and
the check that it is true that is included in the check, and the term "verify"
means exactly that.


> A second (minor) problem is that class-wide postcondition expressions
> are not "inherited"; they "apply", so the phrase "includes class-wide
> postconditions inherited from progenitors of T" is nonsense in
> normative text. (And "class-wide postconditions" is a term that is not
> defined at all). We could say something like "includes class-wide
> postconditions expressions that apply solely because they are defined
> for primitives of progenitors of T", but that seems pretty wordy.
> Still, I don't have a better idea. That gives:
>
>    For any subprogram or entry call (including dispatching calls), the specific
>    precondition check and the postcondition check [Redundant: (which checks both specific
>    and class-wide postcondition expressions, if any)] that are performed are determined by
>    those of the subprogram or entry actually invoked. The postcondition
>    check that is performed on a call of a primitive of type T includes class-wide
>    postcondition expressions that apply solely because they are defined for primitives of
>    progenitors of T [Redundant: , even if the primitive is inherited from a type T1 and
>    these postconditions do not apply to the corresponding primitive of T1].
>
> Any improvements will be appreciated.

Not real happy with that, especially the "apply solely because" part.
How about:

    For any subprogram or entry call (including dispatching calls), the checks
    that are performed that verify specific precondition expressions and
    specific and class-wide postcondition expressions are determined by those
    for the subprogram or entry actually invoked.  Note that the class-wide
    postcondition expressions verified by the postcondition check that is part
    of a call on a primitive of type T includes all class-wide postcondition
    expressions originating in any progenitor of T [Redundant: , even if the
    primitive called is inherited from a type T1 and some of the postcondition
    expressions do not apply to the corresponding primitive of T1].

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

From: Randy Brukardt
Sent: Sunday, July 24, 2011 11:36 PM

I wasn't happy about having to fix it in order to finish that AI, especially at
2 am. And it surely wasn't my best work (whose is at the end of a long day?).

Anyway, I think this is fine and addresses the problems with the previous
version. I'll use it pending any further suggestions.

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

From: Erhard Ploedereder
Sent: Monday, July 25, 2011  5:55 AM

> The checks are performed in an arbitrary order, and if any
> postcondition expression evaluates to False, it is not specified
> whether any other postcondition expressions are evaluated. The
> postcondition checks and constraint checks associated with copying
> back in out or out parameters are performed in an arbitrary order.

I found it "syntactically" strange that we should state omission of subsequent
checks only for postconditions and not for constraint checks. The previous
wording applied to both checks. To fix this, here is a suggested rewrite:

-------------
The evaluation of the postcondition expressions and any constraint checks
associated with copying back in out or out parameters are performed in an
arbitrary order. If any postcondition expression evaluates to False or any
constraint check fails, it is not specified whether any other checks are
evaluated.
--------------

Note that I replaced "postcondition check" by "evaluation of the p.c.e."
The reason is that the manual defined "the postcondition check" as the
combination of these evaluations (see the first two sentences of 6.1.1. (24/3).
Incidently, 22/3 and 23/3 have the same problem for the class-wide precondition
check. It ought to be fixed there, too.

Sideremark: Maybe the term "xx-condition check" should be used for the
evaluation of any inidividual xx-condition expression that applies, rather than
to any combination of them. It would make the wording simpler.

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

From: Bob Duff
Sent: Monday, July 25, 2011  8:20 AM

> I'm definitely in "leave it alone" mode.

Good.

>... I don't think your suggestion works  (everywhere).

My suggestion was for this paragraph alone.

I forgot to reply to this part of your earlier message:

> I don't feel strongly, of course, so if there is a groundswell, I'll
> change it (and should do so in all 29 places, I think).

I am strongly opposed to changing 29 places where wording already exists from
Ada 2005 and before!  JPR suggested a minor change to this particular paragraph,
which IMHO should have no bearing on 29 others.  I'm all for consistency, but
you pointed out that we use both "callable entity" and "subp or entry" all over,
so lets live with that.

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

From: Jean-Pierre Rosen
Sent: Monday, July 25, 2011  9:07 AM

> I am strongly opposed to changing 29 places where wording already
> exists from Ada 2005 and before!  JPR suggested a minor change to this
> particular paragraph, which IMHO should have no bearing on 29 others.
> I'm all for consistency, but you pointed out that we use both
> "callable entity" and "subp or entry" all over, so lets live with
> that.

Agreed.

What happened is that I looked at that paragraph, asked myself "Oh, he didn't
use 'callable entity', is there some subtle difference between 'callable entity'
and 'subp or entry' ?", checked and saw there was none, and therefore suggested
to use the proper term.

If there are 29 of these, forget it.

(apparently the term "callable entity" did not exist in Ada83, it was introduced
with Ada 95, with probably no backward patch)

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

From: Bob Duff
Sent: Monday, July 25, 2011  9:52 AM

> (apparently the term "callable entity" did not exist in Ada83, it was
> introduced with Ada 95, with probably no backward patch)

Right, it didn't exist in Ada 83.

I invented the term "callable entity", because I thought it would simplify
things, and as far as I remember, I intended to switch over to this term
everywhere.  I don't know why there are still occurrences of "subprogram or
entry":  I missed some?  Or some got added since Ada 9X?  Or during Ada 9X, by
people I failed to inform about it? Or the wording works better with "subprogram
or entry" in some places?

Anyway, I don't think we should worry about "fixing" this little inconsistency.

Note that I've gotting closer to the "if it ain't broke, don't fix it"
philosophy, for the RM, since Ada 9X days.  In those days, I was itching to fix
anything that looked like a bug.

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

From: Erhard Ploedereder
Sent: Monday, July 25, 2011  6:04 AM

> A better (maybe?) solution would be for the value of True to be the
> default if and only if no other class-wide precondition "applies" to
> the subprogram; if any other class-wide precondition applies, then
> there is no class-wide precondition directly for this entity (of
> course, the class-wide preconditions that come from ancestors still
> apply).

Indeed.

And as far as the rest of Randy's message goes, that merely enforces my earlier
sideremark about the meaning of "check". We ought to define the xx-checks to
mean the evaluation of any new or "applying" xx expression plus the raising of
the exception as needed. All other texts could then talk in term of failing of
sucessful checks as for all the other checking that goes on.

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

From: Tucker Taft
Sent: Monday, July 25, 2011  6:30 AM

"applying" ==> "applicable".
"sucessful" ==> "successful"

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

From: Randy Brukardt
Sent: Monday, July 25, 2011  9:47 PM

> And as far as the rest of Randy's message goes, that merely enforces
> my earlier sideremark about the meaning of "check".
> We ought to define the xx-checks to mean the evaluation of any new or
> "applying" xx expression plus the raising of the exception as needed.
> All other texts could then talk in term of  failing of sucessful
> checks as for all the other checking that goes on.

"Check" in Ada *never* includes the raising of an exception. See the many, many
places in the Ada Standard where we say "xxx_Error is raised if this check
fails". (Some examples: 13.11.4(27/3), 4.6(57), 4.8(10.1/3), ...)

And as far as the rest of it goes, that's exactly what it says. At least, I
can't see any substantive difference. The only thing we care about (or should
care about, IMHO) is that the postcondition check can be made before or after
the parameters are copied back. There is no need for more flexibility than that.

In any case, what you're asking for is a near complete rewrite of the dynamic
semantics sections of 6.1.1 (and also of 7.3.2, type invariants, which uses the
same wording). Most likely, the rewrite will introduce a new batch of bugs.
(There have been plenty in the existing wording.) And you're asking for it to be
inconsistent with the rest of the Standard. So I'd much prefer to use editor's
discression and ignore this suggestion.

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

From: Randy Brukardt
Sent: Monday, July 25, 2011  9:28 PM

> > The checks are performed in an arbitrary order, and if any
> > postcondition expression evaluates to False, it is not specified
> > whether any other postcondition expressions are evaluated. The
> > postcondition checks and constraint checks associated with copying
> > back in out or out parameters are performed in an arbitrary order.
>
> I found it "syntactically" strange that we should state omission of
> subsequent checks only for postconditions and not for constraint
> checks.

The wording you quoted is wrong anyway, there is only one postcondition check.
(I've fixed that in the wording used in the Standard; it's quite different than
what was in my e-mail.) In any case, what the permission does is allows omitting
part of the check once it has been determined it fails.

A compiler never has to make other checks once one fails -- if we need to say
that explicitly here, there would be a hundred other places in the standard
where we would need to say the same thing. And if none of the checks fails, they
all have to be made. (Constraint checks can't have side effects anyway, so it's
not clear to me that anyone can tell whether they are made when they succeed.)

For one example, the (normal) wording for copy back of parameters (in
6.4.1(17)) says:

After normal completion and leaving of a subprogram, for each in out or out
parameter that is passed by copy, the value of the formal parameter is converted
to the subtype of the variable given as the actual parameter and assigned to it.
These conversions and assignments occur in an arbitrary order.

There is nothing here about omitting checks if one fails. I don't see any reason
that we need to add such wording for postconditions or anywhere else for that
matter.

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

From: Erhard Ploedereder
Sent: Tuesday, July 26, 2011  4:43 AM

> There is nothing here about omitting checks if one fails. I don't see
> any reason that we need to add such wording for postconditions or
> anywhere else for that matter.

Well, my point was that it was there before your rewrite. In the end, we want
short-circuit semantics for the pre-/postcondition checks, no specified order of
the term evaluations and (arguably?) no specified order with constraint checks
on entry and exit.

> there is only one postcondition check

Definitely NOT true in the version of the RM in Edinburgh, which knows of two
postcondition checks: 6.1.1. says
" ... precondition checks are performed as follows:
 The specific precondition check begins with ...
 The class-wide precondition check begins with ....

Now, I don't like that for all the reasons that you cite, but I would go in the
opposite direction and make each expression a check. Then the "no more checks
once the exception is raised" indeed takes care of short-circuit semantics
without the need for extra words.

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

From: Randy Brukardt
Sent: Tuesday, July 26, 2011  5:12 PM

> > There is nothing here about omitting checks if one fails. I
> don't see
> > any reason that we need to add such wording for postconditions or
> > anywhere else for that matter.
>
> Well, my point was that it was there before your rewrite.

OK, and my point was that we don't need it, so it doesn't matter if it is there or not.

> In
> the end, we want short-circuit semantics for the pre-/postcondition
> checks, no specified order of the term evaluations and (arguably?) no
> specified order with constraint checks on entry and exit.

Right.

> > there is only one postcondition check
>
> Definitely NOT true in the version of the RM in Edinburgh, which knows
> of two postcondition checks:
> 6.1.1. says
> " ... precondition checks are performed as follows:
> . The specific precondition check begins with ...
> . The class-wide precondition check begins with ....

Umm, I said there was only one POSTcondition check, and you responded with two
rules about PREcondition checks. Those aren't related (yes, there are multiple
precondition checks, but we were not talking about that rule). [Aside: One of
the big mistakes that we made early on with pre- and postconditions was assuming
that the rules for them could be the same; it turns out that they are wildly
different and very little about them should be the same. That was the lesson of
AI05-0247-1.]

> Now, I don't like that for all the reasons that you cite, but I would
> go in the opposite direction and make each expression a check. Then
> the "no more checks once the exception is raised" indeed takes care of
> short-circuit semantics without the need for extra words.

I think you are so confused now that it would be better if you started over with
the entire clause and reviewed it as a whole (and then decide whether you think
there are any problems). On top of that, you don't even have the current
wording. So I suggest you review the entire clause when the review version of
the Standard comes out in a week or so and we can take this discussion up again
(if necessary) once you've done that.

(I need to get the rest of the Standard done so everyone can review it - the
deadline for starting that review is upon us and I still have a number of days
of work to finish.)

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