!standard 6.1.1(0)                                11-07-22    AI05-0254-1/02
!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

**TBD.

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

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

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 legality rules should be constructed. Possibly,
an ACATS C-Test should be constructed to ensure that postconditions are
evaluated as specified in this wording.

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

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