Version 1.2 of ai05s/ai05-0254-1.txt
!standard 6.3.2(0) 11-06-16 AI05-0254-1/01
!class Amendment 11-06-16
!status work item 11-06-16
!status received 11-06-05
!subject Do we REALLY have contracts right?
The fixes made in AI05-0247-1 have some ARG members uncomfortable.
Should we reconsider? (No.)
[The following is the editor's take:]
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)
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
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 possibly could use 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 (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 would matter.
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...
Questions? Ask the ACAA Technical Agent