CVS difference for ai05s/ai05-0247-1.txt
--- ai05s/ai05-0247-1.txt 2011/04/02 07:30:36 1.5
+++ ai05s/ai05-0247-1.txt 2011/04/16 07:30:08 1.6
@@ -1,4 +1,4 @@
-!standard 13.3.2(19/3) 11-03-28 AI05-0247-1/04
+!standard 13.3.2(0/3) 11-04-15 AI05-0247-1/05
!reference AI05-0145-2
!class Amendment 11-03-21
!status work item 11-03-21
@@ -38,11 +38,11 @@
procedure P1 (Obj : in out I2) is null
with Post'Class => Is_Green (Obj);
procedure P2 (Obj : in I2) is null
- when Pre'Class => Is_Green (Obj);
+ with Pre'Class => Is_Green (Obj);
procedure P3 (Obj : in I2) is null
- when Pre'Class => Is_Green (Obj);
+ with Pre'Class => Is_Green (Obj);
function Something_Green return I2 is abstract
- when Post'Class => Is_Green (Something_Green'Result);
+ with Post'Class => Is_Green (Something_Green'Result);
end Pack2;
with Pack1, Pack2;
@@ -64,10 +64,10 @@
procedure Main is
procedure Do_It (Obj : in out Pack3.T3'Class) is
begin
- Obj.P1; -- (1)
- Obj.P2; -- (2)
+ Pack3.P1(Obj); -- (1)
+ Pack3.P2(Obj); -- (2)
end Do_It;
- O3 : P3.T3;
+ O3 : Pack3.T3;
begin
Do_It (O3);
end Main;
@@ -89,14 +89,15 @@
with Pack2, Pack3;
procedure Main2 is
- procedure Do_It (Obj : in out Pack2.T2'Class) is
+ procedure Do_It (Obj : in Pack2.I2'Class) is
begin
- Obj.P3; -- (3)
+ Pack2.P3(Obj); -- (3)
end Do_It;
begin
- Do_It (P3.Something_Green);
+ Do_It (Pack3.Something_Green);
end Main2;
+
The effective precondition for the call at (3) (assuming that inherited routines
have the same contract aspects as an overriding routine) is Is_Green(Obj) or
Is_Valid(Obj). The call at (3) has to pass its precondition, as Is_Green(Obj)
@@ -107,14 +108,37 @@
(since of course it knows nothing about Is_Green).
-The key to a solution is to realize that Preconditions and Postconditions are
-different and require different rules for dispatching calls. As we noted above,
-getting postconditions to work properly just requires ensuring that in any case
-where a postcondition is added by an interface that the added postcondition is
-reflected in the called routine. Any dispatching call would have to expect the
-same or a weaker postcondition; thus, it is OK for postconditions to be those of
-the body (modulo ensuring that the body evaluates any newly added
-postconditions).
+What we want to ensure is that the classwide preconditions (Pre'Class) and
+classwide postconditions (Post'Class) automatically provide appropriate
+behavior to preserve the Liskov Substitutability Principle (LSP). LSP is
+important because it provides the foundation for proving anything about a
+dispatching call. So long as all of the overridings preserve LSP, the properties
+known for the dispatching call can be assured. On the other hand, if LSP is
+violated, nothing can be assumed about the properties of the dispatching call
+with examining the actual bodies called.
+
+LSP is required by various standards (specifically DO-178C), so it is important
+that Ada have good support for it.
+
+But LSP can get in the way, especially for statically bound calls (where there
+is no benefit). Thus we do not want to put any restrictions on how specific
+preconditions and postconditions are used.
+
+LSP requires that preconditions are combined with "or" (weakening), and
+postconditions are combined with "and" (strengthening), and that they are
+inherited by all overridings. That is the behavior that we want for class-wide
+preconditions and postconditions.
+
+
+Since class-wide preconditions are combined differently than class-wide
+postconditions, it makes sense that they may require different rules.
+In particular, the handling of dispatching calls and subprogram inheritance
+need to be different. As we noted above, getting postconditions to work properly
+just requires ensuring that in any case where a postcondition is added by an
+interface that the added postcondition is reflected in the called routine. Any
+dispatching call would have to expect the same or a weaker postcondition; thus,
+it is OK for postconditions to be those of the body (modulo ensuring that the
+body evaluates any newly added postconditions).
But this does not work for the preconditions of dispatching calls. The only
precondition that the writer of a dispatching call can know about is that of the
@@ -129,11 +153,16 @@
the (implicit) body Pack3.P3. And it is completely different than the
precondition of the (inherited) actual body Pack1.P3 (which is Is_Valid(Obj)).
-The precondition of the inherited routine seems wrong. But that's simply because
-preconditions can't change by inheritance; they have to be rechecked for
-inherited routines. The way to think about what is required is to imagine that
-the inherited routine was in fact written explicitly. In the case of Pack3.P3,
-the body would presumably look like:
+However, the precondition of the inherited routine seems wrong. It is *weaker*
+than the one expected by the invoked body (if the entire inherited precondition
+is considered), and might even be different as noted above. It turns out that
+any such precondition (where a precondition is inherited from multiple,
+different ancestor routines) will always violate LSP unless the inherited
+preconditions are exactly the same.
+
+This should be obvious if one imagines that the inherited routine was in fact
+written explicitly. In the case of Pack3.P3, the body would presumably look
+like:
procedure P3 (Obj : in T3) is
begin
@@ -149,10 +178,15 @@
OTOH, a dispatching call using an object of T1'Class does not need to check
Is_Green at all.
-Note that if we are using Pre rather than Pre'Class, then the preconditions of
-a dispatching call need not have any real relationship. In that case, the existing
-rules are as good as any, and they have the advantage of working the same way
-for access-to-subprogram calls.
+Since this sort of inheritance always will violate LSP, we don't want the
+compiler generating such routines automatically. Thus we introduce a rule
+that such routines require overriding.
+
+Note that if we are using Pre (a specific precondition) rather than Pre'Class
+(a class-wide precondition), then the preconditions of a dispatching call need
+not have any real relationship. In that case, the existing rules are as good as
+any, and they have the advantage of working the same way for
+access-to-subprogram calls.
There are additional problems. While logically preconditions are evaluated at
@@ -180,7 +214,7 @@
expecting.
-Thus we need to make four changes:
+Thus we need to make five changes:
* change the rules for evaluation of Pre preconditions such that they are
evaluated separately from any Pre'Class preconditions (and have to be True
for a call to succeed);
@@ -189,229 +223,370 @@
* change the rules for classwide preconditions of dispatching calls, such that
the precondition of the (denoted) call is evaluated, not the (possibly)
weaker precondition of the invoked body;
- * change the rules for inherited subprograms that have Pre'Class/Post'Class;
+ * add a rule to require overriding if the class-wide precondition is
+ weaker than that of the inherited body(s);
+ * change the rules for inherited subprograms that have Post'Class;
such subprograms are always equivalent to a call on the concrete body (with
- the appropriate preconditions/postconditions evaluated for that call).
+ the appropriate postconditions evaluated for that call).
+We need a similar rule to the last for Type_Invariant'Class.
!wording
+
+Replace 13.3.2 [from AI05-0145-2] with the following:
-Add at the end of 3.10.2(32/2):
+[Editor's note: Parts of this wording, including all of the Static Semantics,
+are unchanged. We put the entire wording here to make it easy to see what
+the entire rules are.]
+
+ 13.3.2 Preconditions and Postconditions
+
+ For a subprogram or entry, the following language-defined aspects may
+ be specified with an aspect_specification:
+ Pre
+ This aspect defines a specific precondition for a callable entity; it
+ shall be specified by an expression, called a *specific precondition
+ expression*. If not specified for an entity, the specific precondition
+ expression for the entity is the enumeration literal True.
+ Pre'Class
+ This aspect defines 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, the class-wide precondition expression for the
+ entity is the enumeration literal True.
+ Post
+ This aspect defines a specific postcondition for a callable entity; it
+ shall be specified by an expression, called a *specific postcondition
+ expression*. If not specified for an entity, the specific postcondition
+ expression for the entity is the enumeration literal True.
+ Post'Class
+ This aspect defines a class-wide postcondition for a callable entity and
+ its descendants; it shall be specified by an expression, called a
+ *class-wide postcondition expression*. If not specified for an entity,
+ the class-wide postcondition expression for the entity is the
+ enumeration literal True.
+
+ Name Resolution Rules
+
+ The expected type for any precondition or postcondition expression is
+ any boolean type.
+
+ Within the expression for a Pre'Class or Post'Class aspect for a primitive
+ subprogram of a tagged type T, a name that denotes a formal parameter of type
+ T is interpreted as having type T'Class. Similarly, a name that denotes a
+ formal access parameter of type access-to-T is interpreted as having type
+ access-to-T'Class. [Redundant: This ensures the expression is
+ well-defined for a primitive subprogram of a type descended from T.]
+
+ For an attribute_reference with attribute_designator Old, if the attribute
+ reference has an expected type or shall resolve to a given type, the same
+ applies to the prefix; otherwise the prefix shall be resolved independently
+ of context.
+
+ Legality Rules
+
+ The Pre or Post aspect shall not be specified for an abstract
+ subprogram. [Redundant: Only the Pre'Class and Post'Class aspects may
+ be specified for such a subprogram.]
+
+ If two or more homographs (see 8.3) that are subprograms are implicitly
+ declared at the same place, and at least one of the homographs is not
+ abstract and has a class-wide precondition expression that applies
+ that is not the enumeration literal True then then the homographs
+ *require overriding* and shall be overridden with a nonabstract subprogram.
+
+[Editor's note: I borrowed a lot of the above wording from 3.9.3(6/2) and
+8.3(12.1-3/2).]
+
+ AARM Reason: Such an inherited subprogram would necessarily violate the
+ Liskov Substitutability Principle (LSP) if called via a dispatching call
+ from the "wrong" ancestor. In such a case, the class-wide precondition of
+ the actual body is stronger than the class-wide precondition of the
+ ancestor. If we did not enforce that precondition for the body, the body
+ could be called when the precondition it knows about is False - such
+ "counterfeiting" of preconditions has to be avoided. But enforcing the
+ precondition violates LSP. We do not want the language to be implicitly
+ creating bodies that violate LSP; the programmer can still write an explicit
+ body that calls the appropriate parent subprogram. In that case, the
+ violation of LSP is explicitly in the code and obvious to code reviewers
+ (both human and automated).
+
+ If a renaming of a subprogram or entry SE overrides an inherited subprogram
+ SI, then the overriding is illegal if SE has a class-wide
+ precondition that applies to it that is not the enumeration literal True.
+
+ AARM Reason: Such an overriding subprogram would violate LSP, as
+ the precondition of SE would usually be different (and thus stronger)
+ than the one known to a dispatching call through an ancestor routine of SI.
+ True is the weakest possible precondition, so we can always allow that.
+
+ AARM Ramification: This only applies to primitives of tagged types;
+ other routines cannot have class-wide preconditions.
+
+**** Notes for Tucker:
+** We could define "conformant preconditions" and use that instead of "True"
+ here (all of the preconditions would have to be conformant). But that is
+ complex; it's similar to full conformance, but the homographs from different
+ ancestors necessarily will not conform (any subprograms will denote different
+ routines as the types are different), even if we make an allowance for
+ the different current-instances. I can show an example if you don't
+ understand this point. I don't think the complexity is worth it.
+** Also note that the "one-sided" checks above only work for True, so far as
+ I can tell. Allowing those specially would add even more to the complexity.
+** I don't see any reason to involve conformance (other than the first
+ note here), as these two are the only such checks that we want. We don't
+ want to make other overridings illegal; we don't want any effect on
+ 'Access; we don't want anything to change for generic formal subprograms
+ or renamings other than the above.
+** These rules have nothing to do with postconditions or invariants. See below.
+*** End Tucker notes.
+
+ Static Semantics
+
+ If a Pre'Class or Post'Class aspect is specified for a primitive
+ subprogram of a tagged type T, then the associated expression also
+ applies to the corresponding primitive subprogram of each descendant
+ of T.
+
+ For a prefix X that denotes an object of a nonlimited type,
+ the following attribute is defined:
+
+ X'Old Denotes the value of X at the beginning of the execution
+ of the subprogram or entry. For each X'Old in a postcondition
+ expression that is enabled, a constant is implicitly declared
+ at the beginning of the subprogram or entry, of the type of X,
+ initialized to X. The value of X'Old in the postcondition
+ expression is the value of this constant. The type of X'Old
+ is the type of X. These implicit
+ declarations occur in an arbitrary order.
+
+ Use of this attribute is allowed only within a postcondition
+ expression.
+
+AARM annotation:
+
+ The prefix X can be any nonlimited object that obeys the syntax for
+ prefix. Useful cases are: the name of a formal parameter of mode
+ '[in] out', the name of a global variable updated by the subprogram,
+ a function call passing those as parameters, a subcomponent
+ of those things, etc.
+
+ A qualified expression can be used to make an arbitrary expression into a
+ valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old
+ is not. The value being saved here is the sum of X and Y (a function
+ result is an object). Of course, in this case "+"(X, Y)'Old is also
+ legal, but the qualified expression is arguably more readable.
+
+ Note that F(X)'Old and F(X'Old) are not necessarily equal.
+ The former calls F(X) and saves that value for later use during
+ the postcondition. The latter saves the value of X,
+ and during the postcondition, passes that saved value
+ to F. In most cases, the former is what one wants.
+
+ If X has controlled parts, adjustment and finalization are implied
+ by the implicit constant declaration.
+
+ If postconditions are disabled, we want the compiler to avoid any
+ overhead associated with saving 'Old values.
+
+ 'Old makes no sense for limited types, because its implementation
+ involves copying. It might make semantic sense to allow
+ build-in-place, but it's not worth the trouble.
+
+end AARM annotation.
+
+ For a prefix F that denotes a function declaration, the following attribute is
+ defined:
+
+ F'Result
+ Within a postcondition expression for function F, denotes
+ the result object of the function. The type of this attribute is that
+ of the function result except within a Post'Class postcondition
+ expression for a function with a controlling result or with a
+ controlling access result. For a controlling result, the type of the
+ attribute is T'Class, where T is the function result type. For a
+ controlling access result, the type of the attribute is an anonymous
+ access type whose designated type is T'Class, where T is the
+ designated type of the function result type. Use of this attribute
+ is allowed only within a postcondition expression for F.
+
+
+ Dynamic Semantics
+
+ If the Assertion_Policy in effect at the point of a subprogram or entry
+ declaration is Check, then upon a call of the subprogram or entry, after
+ evaluating any actual parameters, precondition checks are performed as
+ follows:
+
+ * The specific precondition check begins with the evaluation of the specific
+ precondition expression that applies to the subprogram or entry;
+ if the expression evaluates to False, Assertions.Assertion_Error is raised.
+
+ * The class-wide precondition check begins with the evaluation of any
+ class-wide precondition expressions that apply to the subprogram
+ or entry. If and only if all the class-wide precondition expressions
+ evaluate to False, Assertions.Assertion_Error is raised.
+
+ AARM Ramification: The class-wide precondition expressions of the entity
+ itself as well as those of any parent or progentitor operations are
+ evaluated, as these apply to all descendants.
+
+ The 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. 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.
+
+
+ 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.
+
+ AARM Ramification: The class-wide postcondition expressions of the entity
+ itself as well as those of any parent or progentitor operations are
+ evaluated, as these apply to all descendants; in constrast, only the
+ specific postcondition of the entity applies. Postconditions can always
+ be evaluated inside the invoked body.
+
+
+ If a precondition or postcondition check fails, the exception is
+ raised at the point of the call. [Redundant: The exception cannot
+ be handled inside the called subprogram.]
+
+ For any subprogram or entry call (including dispatching calls), the specific
+ precondition check and the postcondition check that is performed is determined
+ by the those of the subprogram or entry actually invoked.
+
+ AARM Ramification: This applies to access-to-subprogram calls, dispatching
+ calls, and to statically bound calls. We need this rule to cover statically
+ bound calls as well, as specific pre- and postconditions are not inherited,
+ but the subprogram might be. [Editor's note: Wording to define aspect
+ inheritance only in non-overriding situations seems to be way too complex --
+ and we need this rule for dispatching and access-to-subprogram calls
+ anyway.]
+
+ For a call via an access-to-subprogram value, the class-wide precondition
+ check is determined by the subprogram or entry actually invoked.
+ 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).
+
+ AARM Ramification: For a dispatching call, we are talking about the
+ Pre'Class(es) that apply to the subprogram that the dispatching call is
+ resolving to, not the Pre'Class(es) for the subprogram that is ultimately
+ dispatched to. The class-wide precondition of the resolved call is
+ necessarily the same or stronger than that of the invoked call. For a
+ statically bound call, these are the same; for an access-to-subprogram,
+ (which has no class-wide preconditions of its own), we check the
+ class-wide preconditions of the invoked routine.
+
+ AARM Implementation Note: These rules imply that logically, class-wide
+ preconditions of routines must be checked at the point of call (other
+ that for access-to-subprogram calls, which must be checked in the body,
+ probably using a wrapper). Specific preconditions that might be called with
+ a dispatching call or via an access-to-subprogram value must be checked
+ inside of the subprogram body. In contrast, the postcondition checks always
+ need to be checked inside the body of the routine. Of course, an
+ implementation can evaluate all of these at the point of call for statically
+ bound calls if the implementation uses wrappers for dispatching bodies and
+ for 'Access values.
+ End AARM Implementation Note.
+
+
+**** Note to Tucker: The following needs to be replaced by some other rules
+**** for class-wide postconditions and invariants.
+**** Since we don't have any sensible way to describe the situation (this
+**** is a case where the invoked subprogram (if inherited) may have additional
+**** postconditions that need to be evaluated, so the "clean" wording above
+**** does not work.
+**** Moreover, even if we can find a way to describe this for postconditions
+**** (which I grant is possible), I cannot imagine any such wording working
+**** for Type_Invariants (which is a conglomeration of checks).
+**** So I've left this wording until you can come up with a replacement.
+**** (I did prune out the precondition cases.) Enjoy. ;-)
+
+ Notwithstanding what this standard says elsewhere, an inherited subprogram S
+ (or multiple conformant inherited subprograms) that has one or or more
+ class-wide postcondition expressions that apply to S, or has a
+ specified Type_Invariant'Class (see 13.3.3), that is not explicitly
+ overridden, and that is primitive for a type that has one or more progenitors
+ is equivalent to an overriding subprogram S whose body consists of:
+ * The null statement, if all of the inherited subprograms are null
+ procedures;
+ * A call on the parent subprogram, with all of the parameters the same as the
+ parameters to S (possibly with appropriate type conversions on the
+ parameters and result if any).
+
+ AARM Ramification: This equivalence implies that a dispatching
+ call will call this body, rather than that of one of the inherited
+ subprograms. This body will enforce all of the postconditions and type
+ invariants inherited from all of the ancestors. Note that if the routines
+ are not all null, then the subprogram inherited for the parent type must be
+ concrete (not abstract or null), so that is the one we want to call.
+
+ [Editor's Note: We really mean "equivalent", as opposed to the standard use
+ in the standard when it really means something more like "pretty similar".]
+
+ AARM Discussion: Only one implicit overriding subprogram is created for a
+ single set of inherited subprograms that are homographs.
+
+ AARM Reason: These rules eliminate two potential problems: (1) the issue
+ that two null subprograms (one of which is chosen for dispatching
+ arbitrarily by 3.9.2(20.3/3)) might have different aspects that apply,
+ causing different runtime behavior [note that the Legality Rule requiring
+ overriding preconditions also helps solve this problem]; (2) problems that
+ arise because postconditions and invariants added by an interface would not
+ be enforced on an inherited routine (it does not know about any such
+ contracts).
+
+ [Editor's note: We do not need to talk about this in single inheritance cases
+ because the contract aspects cannot change in that case. We do not need to
+ talk about this unless there is a class-wide aspect involved because other
+ aspects (Pre, Post, Type_Invariant) are not inherited. We could have made this
+ apply to all inheritance of routines that can have class-wide aspects, but we
+ didn't do that as that would appear to change the dispatching model (even
+ though compilers would not need to change in the absence of contract
+ aspects).]
+
+**** End wording that is hated by Tucker, but still is the best I can do. :-)
+
+
+ If the Assertion_Policy in effect at the point of a
+ subprogram or entry declaration is Ignore, then no precondition or
+ postcondition check is performed on a call on that subprogram or entry.
+ If the Assertion_Policy in effect at the point of a
+ subprogram or entry declaration is Check, then preconditions and
+ postconditions are considered to be *enabled* for that subprogram or
+ entry.
+
+ Bounded Errors
+
+ It is a bounded error to invoke a potentially blocking operation (see
+ 9.5.1) during the evaluation of a precondition or postcondition expression.
+ If the bounded error is detected, Program_Error is raised. If not detected,
+ execution proceeds normally, but if it is invoked within a protected action,
+ it might result in deadlock or a (nested) protected action.
+
+
+NOTE: A precondition is checked just before the call. If another task can
+change any value that the precondition expression depends on, the precondition
+may not hold within the subprogram or entry body.
-If P has one or more class-wide precondition expressions that apply to it, at least
-one of those expressions shall statically denote the Boolean enumeration literal True.
-AARM Reason: An access-to-subprogram type does not have a class-wide precondition; that
-means no such precondition will be checked. This rule prevents a routine with a stronger
-class-wide precondition from being supplied, as it would not be enforced.
-
-
-Modify 13.3.2(2-5/3):
-
-Pre
-This aspect [specifies]{defines} a {specific} precondition for a callable
-entity; it shall be specified by an expression, called a {specific} precondition
-expression. {If not specified for an entity, the specific precondition
-expression for the entity is the enumeration literal True.}
-
-Pre'Class
-This aspect [specifies]{defines} 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, the
-class-wide precondition expression for the entity is the enumeration literal
-True.}
-
-Post
-This aspect [specifies]{defines} a {specific} postcondition for a callable
-entity; it shall be specified by an expression, called a {specific}
-postcondition expression. {If not specified for an entity, the specific
-postcondition expression for the entity is the enumeration literal True.}
-
-Post'Class
-This aspect [specifies]{defines} a {class-wide} postcondition for a callable
-entity and its descendants; it shall be specified by an expression, called a
-{class-wide} postcondition expression. {If not specified for an entity, the
-class-wide postcondition expression for the entity is the enumeration literal
-True.}
-
-Modify 13.3.2(6/3):
-
-The expected type for [a]{any} precondition or postcondition expression is any
-boolean type.
-
-Change 13.3.2(16/3) from:
-
-If one or more precondition expressions apply to a subprogram or entry, and the
-Assertion_Policy in effect at the point of the subprogram or entry declaration
-is Check, then upon a call of the subprogram or entry, after evaluating any
-actual parameters, a precondition check is performed. This begins with the
-evaluation of the precondition expressions that apply to the subprogram or
-entry. If and only if all the precondition expressions evaluate to False,
-Ada.Assertions.Assertion_Error is raised. The order of performing the checks is
-not specified, and if any of the precondition expressions evaluate to True, it
-is not specified whether the other precondition expressions are evaluated. It is
-not specified whether any check for elaboration of the subprogram body is
-performed before or after the precondition check. It is not specified whether in
-a call on a protected operation, the check is performed before or after starting
-the protected action. For a task or protected entry call, the check is performed
-prior to checking whether the entry is open.
-
-to:
-
-If the Assertion_Policy in effect at the point of a subprogram or entry
-declaration is Check, then upon a call of the subprogram or entry, after
-evaluating any actual parameters, precondition checks are performed as follows:
-
-* The specific precondition check begins with the evaluation of the specific
- precondition expression that applies to the subprogram or entry; if the
- expression evaluates to False, Assertions.Assertion_Error is raised.
-
-* The class-wide precondition check begins with the evaluation of any class-wide
- precondition expressions that apply to the subprogram or entry. If and only if
- all the class-wide precondition expressions evaluate to False,
- Assertions.Assertion_Error is raised.
-
-AARM Ramification: The class-wide precondition expressions of the entity itself
-as well as those of any parent or progentitor operations are evaluated, as these
-apply to all descendants.
-
-The 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. 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.
-
-
-Change 13.3.2(17.3) from:
-
-If one or more postcondition expressions apply to a subprogram or entry, and the
-Assertion_Policy in effect at the point of the 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, a postcondition
-check is performed. This consists of the evaluation of the 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 one of them
-evaluates to False, it is not specified whether the 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 check.
-
-to:
-
-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.
-
-AARM Ramification: The class-wide postcondition expressions of the entity itself
-as well as those of any parent or progentitor operations are evaluated, as these
-apply to all descendants; in constrast, only the specific postcondition of the
-entity applies.
-
-
-Change 13.3.2(19/3) from:
-
-For a dispatching call or a call via an access-to-subprogram value, the
-precondition or postcondition check performed is determined by the subprogram
-actually invoked. Redundant[Note that for a dispatching call, if there is a
-Pre'Class aspect that applies to the subprogram named in the call, then if the
-precondition expression for that aspect evaluates to True, the precondition
-check for the call will succeed.]
-
-to:
-
-For any subprogram or entry call (including dispatching calls), the specific
-precondition check and the postcondition check that is performed is
-determined by the those of the subprogram or entry actually invoked.
-
-AARM Ramification: This applies to access-to-subprogram calls, dispatching calls,
-and to statically bound calls. We need this rule to cover statically bound calls
-as well, as specific pre- and postconditions are not inherited, but the
-subprogram might be. [Editor's note: Wording to define aspect inheritance only in
-non-overriding situations seems to be way too complex -- and we need this rule
-for dispatching and access-to-subprogram calls anyway.]
-
-In contrast, 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 entity (not necessarily the one that is invoked).
-
-AARM Ramification: For a dispatching call, we are talking about the Pre'Class(es)
-that apply to the subprogram that the dispatching call is resolving to, not the
-Pre'Class(es) for the subprogram that is ultimately dispatched to. For a statically
-bound call, these are the same; for an access-to-subprogram (which has no
-class-wide preconditions), no class-wide precondition check is needed at all.
-
-AARM Implementation Note: These rules imply that logically, class-wide preconditions
-of routines must be checked at the point of call. Specific preconditions that
-might be called with a dispatching call or via an access-to-subprogram value
-must be checked inside of the subprogram body. In contrast, the postcondition
-checks always need to be checked inside the body of the routine. Of course,
-an implementation can evaluate all of these at the point of call for statically
-bound calls if the implementation uses wrappers for dispatching bodies and for
-'Access values.
-End AARM Implementation Note.
-
-Notwithstanding what this standard says elsewhere, an inherited subprogram S
-(or multiple conformant inherited subprograms) that has one or or more
-class-wide precondition or postcondition expressions that apply to S,
-or has a specified Type_Invariant'Class (see 13.3.3),
-that is not explicitly overridden, and that is primitive for a type that has one
-or more progenitors is equivalent to an overriding subprogram S whose body consists of:
- * The null statement, if all of the inherited subprograms are null procedures;
- * A call on the parent subprogram, with all of the parameters the same as
- the parameters to S (possibly with appropriate type conversions on the parameters
- and result if any).
-
-If a subprogram renaming overrides one or more inherited subprograms, the renaming
-is equivalent of a subprogram whose body calls the renamed subprogram, with all
-of the parameters the same as the parameters to S (possibly with appropriate type
-conversions on the parameters and result if any).
-
-AARM Ramification: This equivalence implies that the call on the parent
-subprogram will evaluate preconditions as needed. And that a dispatching call will
-call this body, rather than that of one of the inherited subprograms. Note that
-if the routines are not all null, then the subprogram inherited for the parent
-type must be concrete (not abstract or null), so that is the one we want to call.
-
-[Editor's Note: We really mean "equivalent", as opposed to the standard use
-in the standard when it really means something more like "pretty similar".]
-
-AARM Discussion: Only one implicit overriding subprogram is created for a single
-set of inherited subprograms that are homographs.
-
-AARM Reason: These rules eliminate four potential problems: (1) the issue that two
-null subprograms (one of which is chosen for dispatching arbitrarily by
-3.9.2(20.3/3)) might have different aspects that apply, causing different runtime
-behavior; (2) "counterfeiting" problems that arise because adding an interface
-precondition to the mix weakens the class-wide precondition of the inherited routine
-(in this case, we need to enforce the class-wide precondition of the actual body,
-else it might not be true when the call is made -- which would be bad); (3) problems
-that arise because postconditions and invariants added by an interface would not be
-enforced on an inherited routine (it does not know about any such contracts);
-(4) problems with the "wrong" class-wide precondition being enforced
-for an overriding rename of a routine that has its own class-wide
-precondition.
-
-[Editor's note: We do not need to talk about this in single inheritance
-cases (other than the renames one) because the contract aspects cannot change in
-that case. We do not need to talk about this unless there is a class-wide aspect
-involved because other aspects (Pre, Post, Type_Invariant) are not inherited.
-We could have made this apply to all inheritance of routines that can have
-class-wide aspects, but we didn't do that as that would appear to change the
-dispatching model (even though compilers would not need to change in the
-absence of contract aspects).]
+
!discussion
This issue originally came up because null procedures are considered the same
@@ -436,25 +611,25 @@
The change to separate Pre from Pre'Class introduces additional problems with
renames and 'Access. Since renaming can change the dispatching status of a
subprogram (from dispatching to statically bound, or the reverse), it introduces
-some interesting problems. This is fixed by applying the "implicit body model" to
-overriding renames.
+some interesting problems. This is fixed by making such overridings illegal.
We also would like access-to-subprogram to work the same way as a dispatching
-call. But that only works if the designated subprogram does not have any Pre'Class
-(as we don't have any such preconditions on access-to-subprogram types). We fix that
-by making 'Access illegal if any significant class-wide precondition applies to
-the subprogram. (We could have used the "implicit body model" here as well.)
+call. But that only works if the designated subprogram does not have any
+Pre'Class (as we don't have any such preconditions on access-to-subprogram
+types). We fix that by making 'Access illegal if any significant class-wide
+precondition applies to the subprogram. (We could have used the "implicit body
+model" here as well.) ***??
We could have solved the Pre/Post inheritance problem by changing the model of
-inheritance in Ada to always generate an implicit body as in the wording proposed
-at the end of the AI. As well as solving that problem, it also would simplify the
-model of dispatching a lot (there would always be a body defined for each type,
-there would never need to be any looking at parents or progenitors for bodies).
-But this would be a substantial change in the presentation of Ada (even though
-it is unlikely that compilers would have to actually generate such bodies in most
-cases). As such it seems like a likely way to inject new bugs into the language --
-and thus it was rejected.
+inheritance in Ada to always generate an implicit body as in the wording
+proposed at the end of the AI. As well as solving that problem, it also would
+simplify the model of dispatching a lot (there would always be a body defined
+for each type, there would never need to be any looking at parents or
+progenitors for bodies). But this would be a substantial change in the
+presentation of Ada (even though it is unlikely that compilers would have to
+actually generate such bodies in most cases). As such it seems like a likely way
+to inject new bugs into the language -- and thus it was rejected.
!corrigendum 13.3.2(0)
@@ -606,7 +781,7 @@
procedure P1 (Obj : in out I2) is null
with Post'Class => Is_Wobbly (I2);
procedure P2 (Obj : in I2) is null
- when Pre'Class => Is_Wobbly (I2);
+ with Pre'Class => Is_Wobbly (I2);
end P2;
with P1, P2;
@@ -779,7 +954,7 @@
procedure P (Obj : in out I2) is null
with Pre'Class => Is_Wobbly (I2);
function Something_Wobbly return I2
- when Post'Class => Is_Wobbly (Something_Wobbly'Result);
+ with Post'Class => Is_Wobbly (Something_Wobbly'Result);
end P2;
with P1, P2;
@@ -4884,6 +5059,26 @@
****************************************************************
+From: Robert Dewar
+Sent: Tuesday, March 29, 2011 8:40 AM
+
+>>> Assume that Visible.Draw is only supported for Visible windows.
+>> Well, there goes Liskov substitutability.
+>
+> I suppose, but I don't much care about ivory-tower principles. If you
+> have this problem (an added property affecting existing operations),
+> you need a mechanism to solve it. That's especially true if you are
+> extending an existing type whose specifications you can't change - I
+> don't think there is any way to preverve the Liskov property in that
+> case. (Raising some random exception rather than writing a proper
+> precondition doesn't change
+> anything.)
+
+Hardly an ivory-tower principle given that DO-178C is likely to require the use
+and verification of LSP in OO contexts
+
+****************************************************************
+
From: Randy Brukardt
Sent: Tuesday, March 29, 2011 1:03 AM
@@ -5087,3 +5282,1770 @@
****************************************************************
+From: Jean-Pierre Rosen
+Sent: Friday, April 1, 2011 4:51 AM
+
+Sorry for entering this discussion late, but I spent the week-end skiing (Hi,
+Tuck), and changed my laptop, which means wasting hours fighting drivers that
+are incompatible between WXP/32 and W7/64...
+
+But OOP is a topic I'm interested in (unlike accessibility rules;-)), so here is
+my point of view.
+
+1) There is an important political issue here. As Robert pointed out, we are in
+ the context of an emerging DO178C. The OO annex is pushed by people who want
+ to introduce Java and C++ in avionics software, and they claim that the
+ complexity of testing dynamic dispatching can be harnessed by strict usage of
+ the LSP (whether this is true is still to be seen, and is irrelevant here).
+ If we manage to /better/ support the LSP than C++ and Java, this will be one
+ more reason to prefer Ada, and we'll have an opportunity to backfire the
+ Java-in-avionics people. If we invent some new concepts for assertions,
+ different from what the LSP needs, we will be shooting ourself in the foot,
+ and providing new good arguments for avoiding Ada in avionics (hey, those
+ guys missed the boat once again!).
+
+Note that I am /not/ a big fan of OOP, and certainly not of OOP everywhere. The
+title of my position paper for the Ada-Europe panel is "Object Orientation in
+Critical Systems: Yes, in Moderation".
+
+2) Interfaces are really a promise to provide some functionalities. To me, they
+ have a value because they are /not/ inheritance (i.e., they don't imply an
+ "is a" relationship), although they might be used that way. Typical use of
+ interfaces is for things like the listener paradigm: register an On_Event
+ subprogram that is called when the event happens, irrespectively of the true
+ type of the supporting object.
+
+3) I fully agree with Bob here:
+> A precondition is a promise made by the caller to the callee.
+> A postcondition is a promise made by the callee to the caller.
+>
+> Or, equivalently:
+> A precondition is a requirement on the caller, which the body can rely on.
+> A postcondition is a requirement on the body, which the caller can rely on.
+
+The important thing is that the precondition is necessary to the algorithm in
+the /body/. A Divide might tell: "sorry, I don't know how to perform this
+service if the rhs is 0, you have to check". A derived Divide that handles
+infinities may accept 0. If the caller doesn't know wich kind of divide it is
+using (due to dispatching), it has to check for 0.
+
+But then, does it make sense to allow (class-wide) preconditions on interfaces?
+Such things have no body! There is no reason to impose checks to the user if
+there is no related algorithmic constraint that requires that check. Putting
+preconditions on (a primitive operation of) an interface is like saying: "we
+assume that future implementations will have a problem if this does not hold".
+
+OTOH, preconditions on interfaces can be understood the other way round (think
+of the listener call-back): a promise from the caller to the implementer that
+some condition holds; whether the implementer needs that condition or not is the
+implementer's problem.
+
+In any case, if a SP is called through a dispatching call of an interface, only
+the preconditions for the interface (if any!) should be checked at the caller
+site. If we have a class-wide precondition on the actual body, raise
+Assertion_Error from the body, just like for a specific precondition. The whole
+point of interfaces is to mix completely unrelated type, therefore there is no
+common requirement on the caller.
+
+Does it defeat static analysis? Yes, but as in Randy's example, that's because
+an implementation of an interface that has some extra preconditions does not
+satisfy the LSP. Such an implementation would be forbidden by the current trend
+of DO178C. Or if you prefer, this works perfectly well as long as you obey the
+LSP. If you don't, the behavior is well specified, but don't expect to prove or
+optimize anything.
+
+Another interesting issue is what happens when you have a dispatching call to a
+primitive operation (through its controlling tagged type) that happens to
+implement an operation of an interface. I would say: don't check the
+preconditions of the interface. If the implementation of the operation requires
+the condition from the interface, it should repeat it in its own preconditions
+(otherwise, it is lying about its real preconditions - something like the
+clauses in tiny characters at the bottom of contracts). If the implementation
+does /not/ require the condition from the interface, there is no point in
+enforcing it. Of course, this would be easier to explain if preconditions on
+interfaces are simply forbidden.
+
+In short, my position is:
+- at the caller's site, check the preconditions that apply to the view of the
+ controlling operand, nothing else. Other conditions that may apply (whether
+ specific or class-wide) are checked in the body.
+- I am still unsure whether preconditions on interfaces should be allowed at
+ all. If it simplifies implementation to forbid them, I could live with it.
+
+Of course, all this discussion does not apply to postconditions, as often noted
+before.
+
+4) I think we should specify whether the evaluation of preconditions on a PO is
+ part of the protected action or not. Otherwise, if the evaluation involves
+ calls to some other PO, we would have a situation where whether the
+ evaluation of preconditions is potentially blocking would depend on the
+ implementation.
+
+5) Some nitpicking:
+> type I2 is interface;
+> function Is_Green (Obj : I2) return Boolean is abstract;
+> procedure P1 (Obj : in out I2) is null
+> with Post'Class => Is_Green (Obj);
+> procedure P2 (Obj : in I2) is null
+> when Pre'Class => Is_Green (Obj);
+ ^^^^ => with
+> procedure P3 (Obj : in I2) is null
+> when Pre'Class => Is_Green (Obj);
+ ^^^^ => with
+> function Something_Green return I2 is abstract
+> when Post'Class => Is_Green (Something_Green'Result);
+ ^^^^ => with
+> end Pack2;
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, April 1, 2011 10:56 AM
+
+> 2) Interfaces are really a promise to provide some functionalities. To
+> me, they have a value because they are /not/ inheritance (i.e., they
+> don't imply an "is a" relationship), although they might be used that
+> way. Typical use of interfaces is for things like the listener
+> paradigm: register an On_Event subprogram that is called when the event
+> happens, irrespectively of the true type of the supporting object.
+
+> ...
+> But then, does it make sense to allow (class-wide) preconditions on
+> interfaces? Such things have no body! There is no reason to impose
+> checks to the user if there is no related algorithmic constraint that
+> requires that check. Putting preconditions on (a primitive operation
+> of) an interface is like saying: "we assume that future implementations will
+> have a problem if this does not hold".
+
+> OTOH, preconditions on interfaces can be understood the other way
+> round (think of the listener call-back): a promise from the caller to
+> the implementer that some condition holds; whether the implementer needs that
+> condition or not is the implementer's problem. ...
+
+Well you seem to be nicely arguing both sides here. If you think about the
+Listener interface, a class-wide precondition makes perfect sense if it refers
+to the properties of the parameters that are required for a call to make any
+sense. Suppose we have a stream-like interface, which has Open, Is_Open, Read,
+and Close, operations. Clearly we would want a Pre'Class on Read that
+Is_Open(Stream). Similarly for the Listener interface, if you have Subscribe,
+Unsubscribe, and Is_Subscribed, you would want to specify Pre'Class of
+Is_Subscribed(Listener) on the Unsubscribe operation. I don't see anything
+about interfaces that makes preconditions of less value.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Friday, April 1, 2011 11:47 AM
+
+I agree. Preconditions on interfaces make sense if you view them the other way
+round (compared to tagged types): they are not a requirement from the
+implementation, they are a promise to the implementer.
+
+My point is that:
+1) They should not be mixed with other class-wide preconditions. If you dispatch
+ from the interface, checking other preconditions is the responsability of the
+ body. If you dispatch from the tagged type, ignore the preconditions on the
+ interface.
+
+2) If that seems too complicated, I could accept forbidding preconditions on
+ interfaces altogether.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, April 1, 2011 2:03 PM
+
+...
+> I agree. Preconditions on interfaces make sense if you view them the
+> other way round (compared to tagged types): they are not a requirement
+> from the implementation, they are a promise to the implementer.
+
+This is really the wrong way to look at preconditions (and postconditions) at
+all.
+
+These are both *contracts* between the caller and callee; and both are bound
+equally.
+
+Specifically, a class-wide precondition is a contract that puts requirements on
+*any possible* caller when calling *any possible* callee.
+
+If the call in question is statically bound, then the *any possible* doesn't
+have any effect, and the effect is solely on the caller.
+
+But in a dispatching call, the "any possible callee" remains, and that does have
+the effect of a restriction on possible bodies. That has nothing to do with
+interfaces -- it is true of any body of a routine that can be called via a
+dispatching call.
+
+And that makes sense: the class-wide precondition is part of the contract of a
+routine, and as such it puts requirements on both sides.
+
+> My point is that:
+> 1) They should not be mixed with other class-wide preconditions. If
+> you dispatch from the interface, checking other preconditions is the
+> responsability of the body. If you dispatch from the tagged type,
+> ignore the preconditions on the interface.
+
+This is effectively "and"ing them together. But it doesn't make much sense.
+
+Moreover, it demolishes LSP for interfaces.
+
+You said earlier:
+
+> If we invent some new concepts for assertions, different from what the
+> LSP needs, we will be shooting ourself in the foot, and providing new
+> good arguments for avoiding Ada in avionics (hey, those guys missed
+> the boat once again!).
+
+So I can't reconcile these two positions. You're specifically saying "let's get
+it wrong" for interfaces.
+
+Beyond that, I'm strongly opposed to any semantics that denies compilers and
+tools without full source code the ability to do analysis.
+
+> 2) If that seems too complicated, I could accept forbidding
+> preconditions on interfaces altogether.
+
+That doesn't help; in fact, it makes it worse (from the perspective of LSP).
+If there is no precondition, that is equivalent to a precondition of True.
+When you combine that with any other precondition, you end up with True. I don't
+see how that helps anything at all.
+
+I agree that these semantics will make interfaces very hard to use with
+preconditions. But that problem exists in Eiffel and other languages and it
+doesn't seem to bother Meyer or others. Why should we care? We're not going to
+invent a new theory of multiple inheritance in the ARG, and even if we did, no
+one would care.
+
+As Bob pointed out, most use of interfaces is with "root" types. The interfaces
+aren't added to existing trees (that's when the problems happen). And they're
+not usually added to inherited operations, but rather new ones for the type. It
+would be easy enough to avoid such mix-ins if they cause trouble (we could even
+make them illegal, by requiring overriding in those cases).
+
+Tucker has suggested (and I wrote up) a model where Pre'Class, Post'Class, and
+Type_Invariant'Class preserve LSP everywhere, while Pre, Post, and
+Type_Invariant are free-form. This has the distinct advantage that a simple tool
+like AdaControl can enforce the use of LSP when that is desired (simply ban the
+use of Pre and Post on primitives of a tagged type, and Type_Invariant on tagged
+types). That seems like a major advantage for the avionics people.
+
+If supporting LSP is important (and it sounds like it is), then we can't go
+blowing up LSP for interfaces.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 2:15 PM
+
+> And thanks for reading this and making an attempt to understand it.
+
+You're welcome.
+
+The homework deadline approaches, so I'm about to overwhelm you with emails
+about the homework. Sorry about that!
+
+Please don't feel too overwhelmed about the deadlines!
+WG9 has no power to arrest you if we're late.
+Ada 95 was supposed to be Ada 93.
+Ada 2005 was standardized in 2007.
+If Ada 2012 is a few months late, I promise you that the sky will not fall!
+
+> Bob Duff writes:
+> > I have a feeling we're re-treading the same ground covered by Meyer
+> > / Eiffel.
+>
+> Probably, but Ada also has legacy issues that aren't necessarily
+> present in Eiffel.
+
+Right. We also have to adjust "Eiffel think" to the fact that Ada splits T from
+T'Class, and splits packages from classes/types.
+
+>... In particular, we have to do something useful for existing code
+>that doesn't have preconditions defined.
+
+Right. Clearly the default Pre and Pre'Class has to be True for that reason.
+And of course you can't weaken True.
+
+> > I think this AI addresses some major concerns I had several months
+> > ago (but never got around to bringing up, because I didn't fully
+> > understand the issues).
+>
+> Good to hear.
+>
+> ...
+> > > with Pack1, Pack2;
+> > > package Pack3 is
+> > > type T3 is new Pack1.T1 and Pack2.I2 with private;
+> > > overriding
+> > > function Is_Green (Obj : T3) return Boolean;
+> > > overriding
+> > > procedure P2 (Obj : in T3);
+> > > overriding
+> > > function Something_Green return T3;
+> > > -- P1 and P3 are inherited from Pack1.P1 and Pack1.P3,
+> > > -- respectively.
+> >
+> > Not "respectively". The Pack1 versions override in both cases.
+>
+> Not sure what you mean here. I meant P1 is inherited from Pack1.P1,
+> and P3 is inherited from Pack1.P3.
+
+But, looking back at the original example, that's not true.
+P1 is inherited from both Pack1 and Pack3.
+P3 is inherited from both Pack1 and Pack3.
+The body ones (both in P1) win.
+
+>...Pack2 is not mentioned, and I wasn't interested in the details as
+>to why (irrelevant for this AI). I suppose I could have written this
+>as two separate comments, but I fail to see anything wrong with the
+>one I have.
+
+Well, either it's wrong, or I don't understand it.
+
+> > I wonder if these sorts of examples would be clearer if we avoid
+> > prefix notation calls?!
+>
+> Unless you want to confuse the heck out of yourself, you'll never use
+> prefix calls for dispatching in Ada 2005 or later.
+
+I don't much like prefix calls, either.
+
+> ...The alternative is lots of use
+> clauses (which is not going to help make these examples more
+> understandable), or lengthy prefixes which are really hard to get right.
+> (And I'm not quite sure what the prefix needs to be here...)
+
+Now I don't understand -- you don't like prefix notation, you don't like use
+clauses, and you don't like expanded names. What else is there?
+
+In these examples, I strongly prefer expanded names!
+They're not "lengthy" (here).
+
+Anyway, I'll send you updated examples in a separate message.
+
+> > "shall statically denote True"?
+>
+> A precondition aspect represents an expression, not a value.
+
+"True" is an expression!
+
+>...Thus, we have
+> to word this in terms of the expression, not the value that we might
+>evaluate it to have. In particular, my intent was to require that this
+>expression is exactly the Boolean enumeration literal True. I suppose
+>it would be OK to have used "statically denotes" instead (that allows
+>renames of True):
+>
+> shall statically denote the Boolean enumeration literal True.
+
+It's still needlessly verbose. Think: If someone reads "shall statically
+denote True", what might they think they can write, which you don't want to
+allow?
+
+> > "enumeration literal True" --> "True" (and below)
+>
+> See above. This is *not* a value, but an expression consisting of
+> nothing but the Boolean enumeration literal True. I figured I could
+> leave out "Boolean" since that is the type of the expression, but the
+> other part is necessary to emphasize the distinction.
+
+See MY comment above.
+
+> ...
+>
+> > > Modify 13.3.2(6/3):
+> > >
+> > > The expected type for [a]{any} precondition or postcondition
+> > > expression is any boolean type.
+> >
+> > I think "a" is just as clear.
+>
+> OK, but I disagree; there are two different preconditions, and we
+> never defined "precondition expression" to mean both kinds. That
+> seemed like overkill, so I used "any" consistently to mean all of the kinds.
+
+I still think you're being overly pedantic, but I don't want to fight too much
+over 2 letters. ;-)
+
+> > "task or protected entry call" --> "entry call"
+> >
+> > > performed
+> > > prior to checking whether the entry is open.
+>
+> That's existing Tucker wording which I left unchanged. I assume he was
+> reinforcing some idea here (probably the intent that it applies to
+> both) with the redundancy.
+
+Well, whoever wrote it, I think we can assume that readers know that "entry"
+means "protected or task entry" in Ada!
+
+> ...
+> > > 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 checks is performed. This
+ ^^
+ ||
+> > consists
+> > > of the evaluation of the
+> >
+> > "are"
+>
+> "is". :-). More accurately, "postcondition check is" - there is only
+> one postcondition check (everything is lumped together because there
+> is no need to talk about them individually). I for a while had
+> separated the checks, but I obviously left some vestige of that model when I
+> switched it back.
+
+No, I meant the above marked "checks is" should be "checks are".
+
+> ...
+> > > Notwithstanding what this standard says elsewhere, an inherited subprogram S
+> > > (or multiple conformant inherited subprograms) that has one or or
+> > > more class-wide precondition or postcondition expressions that
+> > > apply to S, or has a specified Type_Invariant'Class (see 13.3.3),
+> > > that is not explicitly overridden, and that is primitive for a
+> > > type that has
+> > > one or more progenitors is equivalent to an overriding subprogram
+> > > S whose
+> > > body consists of:
+> > > * The null statement, if all of the inherited subprograms are
+> > > null subprograms;
+> > > * A call on the parent subprogram, with all of the parameters
+> > > the same
+> > > as the parameters to S (possibly with appropriate type conversions).
+> >
+> > Do we need, "The same rule applies to functions (possibly with
+> > appropriate type conversion of the result)"?
+>
+> Why? This wording is about primitive *subprograms*, and those surely
+> include functions with controlling results. The type conversion
+> wording can be read to apply to everything. I could see expanding that
+> a bit to say "(possibly with appropriate type conversions on the
+> parameters and result if any)", but that's all that could be needed.
+
+OK.
+
+...
+> > > null subprograms (one of which is chosen for dispatching arbitrarily by
+> > > 3.9.2(20.3/3)) may not be equivalent at runtime; (2) "counterfeiting"
+> >
+> > "may not be equivalent at runtime" --> "might have different
+> > contracts"?
+>
+> "contract" is not an RM technical term (at least in this sense), so I
+> didn't want to use that term here. "might have different Pre'Class,
+> Post'Class, and Type_Invariant'Class aspects" is better, but the
+> latter part is possibly confusing.
+>
+> "might have different contract aspects that apply" would be better,
+> but again "contract aspects" is a term that isn't defined.
+>
+> "might have different aspects that apply" seems vague. Besides, the
+> fact that there could be different behavior for two null subprograms
+> is the crux of the issue and needs to be mentioned somehow.
+>
+> I used "might have different aspects that apply, causing different
+> runtime behavior", but there might be something better possible.
+
+OK.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 2:16 PM
+
+>...[AI05-0247-1 Preconditions, Postconditions, multiple inheritance, and
+> dispatching calls]
+
+Here are two copies of the examples from AI05-0247-1, from the !proposal
+section. The first just has some corrections, so it compiles under GNAT:
+
+ I added private parts so it could compile. (You can delete these.)
+ I changed "when" to "with" in several places.
+ In Main2, T2 should be I2.
+ In Main2, P3.Something_Green should be Pack3.Something_Green
+ In Main2, remove "with Pack1;".
+
+ I added explicit conversions to I2'Class in 3 places,
+ because GNAT apparently does not yet implement the rule
+ that these conversions are implicit. These are marked "???NYI",
+ and I suppose you should delete them.
+
+The second one below is identical to the first one, except it uses expanded name
+notation instead of prefix notation. For examples like this, I think that's much
+clearer; I suggest you replace the example in the AI with the second one below.
+
+ package Pack1 is
+ type T1 is tagged private;
+ function Is_Valid (Obj : T1) return Boolean;
+ procedure P1 (Obj : in out T1);
+ procedure P3 (Obj : in T1)
+ with Pre'Class => Is_Valid (Obj);
+ private
+ type T1 is tagged null record;
+ end Pack1;
+
+ package Pack2 is
+ type I2 is interface;
+ function Is_Green (Obj : I2) return Boolean is abstract;
+ procedure P1 (Obj : in out I2) is null
+ with Post'Class => Is_Green (I2'Class(Obj)); -- ???NYI
+ procedure P2 (Obj : in I2) is null
+ with Pre'Class => Is_Green (I2'Class(Obj)); -- ???NYI
+ procedure P3 (Obj : in I2) is null
+ with Pre'Class => Is_Green (I2'Class(Obj)); -- ???NYI
+ function Something_Green return I2 is abstract
+ with Post'Class => Is_Green (Something_Green'Result);
+ end Pack2;
+
+ with Pack1, Pack2;
+ package Pack3 is
+ type T3 is new Pack1.T1 and Pack2.I2 with private;
+ overriding
+ function Is_Green (Obj : T3) return Boolean;
+ overriding
+ procedure P2 (Obj : in T3);
+ overriding
+ function Something_Green return T3;
+ -- P1 and P3 are inherited from Pack1.P1 and Pack1.P3,
+ -- respectively.
+ private
+ type T3 is new Pack1.T1 and Pack2.I2 with null record;
+ end Pack3;
+
+ with Pack1, Pack3;
+ procedure Main is
+ procedure Do_It (Obj : in out Pack3.T3'Class) is
+ begin
+ Obj.P1; -- (1)
+ Obj.P2; -- (2)
+ end Do_It;
+ O3 : Pack3.T3;
+ begin
+ Do_It (O3);
+ end Main;
+
+ ----------------------------------------------------------------
+
+ with Pack2, Pack3;
+ procedure Main2 is
+ procedure Do_It (Obj : in Pack2.I2'Class) is
+ begin
+ Obj.P3; -- (3)
+ end Do_It;
+ begin
+ Do_It (Pack3.Something_Green);
+ end Main2;
+
+ ----------------------------------------------------------------
+
+Here's the second one:
+
+ package Pack1 is
+ type T1 is tagged private;
+ function Is_Valid (Obj : T1) return Boolean;
+ procedure P1 (Obj : in out T1);
+ procedure P3 (Obj : in T1)
+ with Pre'Class => Is_Valid (Obj);
+ private
+ type T1 is tagged null record;
+ end Pack1;
+
+ package Pack2 is
+ type I2 is interface;
+ function Is_Green (Obj : I2) return Boolean is abstract;
+ procedure P1 (Obj : in out I2) is null
+ with Post'Class => Is_Green (I2'Class(Obj)); -- ???NYI
+ procedure P2 (Obj : in I2) is null
+ with Pre'Class => Is_Green (I2'Class(Obj)); -- ???NYI
+ procedure P3 (Obj : in I2) is null
+ with Pre'Class => Is_Green (I2'Class(Obj)); -- ???NYI
+ function Something_Green return I2 is abstract
+ with Post'Class => Is_Green (Something_Green'Result);
+ end Pack2;
+
+ with Pack1, Pack2;
+ package Pack3 is
+ type T3 is new Pack1.T1 and Pack2.I2 with private;
+ overriding
+ function Is_Green (Obj : T3) return Boolean;
+ overriding
+ procedure P2 (Obj : in T3);
+ overriding
+ function Something_Green return T3;
+ -- P1 and P3 are inherited from Pack1.P1 and Pack1.P3,
+ -- respectively.
+ private
+ type T3 is new Pack1.T1 and Pack2.I2 with null record;
+ end Pack3;
+
+ with Pack1, Pack3;
+ procedure Main is
+ procedure Do_It (Obj : in out Pack3.T3'Class) is
+ begin
+ Pack3.P1(Obj); -- (1)
+ Pack3.P2(Obj); -- (2)
+ end Do_It;
+ O3 : Pack3.T3;
+ begin
+ Do_It (O3);
+ end Main;
+
+ ----------------------------------------------------------------
+
+ with Pack2, Pack3;
+ procedure Main2 is
+ procedure Do_It (Obj : in Pack2.I2'Class) is
+ begin
+ Pack2.P3(Obj); -- (3)
+ end Do_It;
+ begin
+ Do_It (Pack3.Something_Green);
+ end Main2;
+
+ ----------------------------------------------------------------
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 2:18 PM
+
+> I'm pretty much of the opinion that this is truly a case-by-case situation.
+> Let me show you the example that I have been thinking about where
+> "weakening" is exactly wrong. Probably there is something wrong with
+> my OOP design, but I can't quite imagine what it would be.
+
+Here, you are deliberately violating LSP. That's not necessarily bad design.
+In fact, I don't think it's possible/feasible to obey LSP in all cases; LSP
+definitely has its problems.
+
+You are strenthening the Pre'Class on derivation.
+I think you said you shouldn't weaken Pre'Class but should leave it the same.
+
+So use Pre instead of Pre'Class. I think you said this in a later email.
+
+> package Root is
+> type Root_Window is limited tagged private;
+>
+> function Exists (W : in Root_Window) return Boolean;
+>
+> procedure Draw (W : in Root_Window; What : Drawing)
+> with Pre'Class => Exists (W));
+> end Root;
+>
+> with Root; use Root;
+> package Visible is
+> type Visible_Window is new Root_Window with private;
+>
+> function Is_Visible (W : in Visible_Window) return Boolean;
+>
+> procedure Show (W : in Visible_Window)
+> with Pre'Class => Exists (W),
+> Post'Class => Is_Visible (W);
+>
+> procedure Draw (W : in Visible_Window; What : Drawing)
+> with Pre'Class => Is_Visible (W);
+> end Visible;
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 2:18 PM
+
+> > > Assume that Visible.Draw is only supported for Visible windows.
+> > Well, there goes Liskov substitutability.
+>
+> I suppose, but I don't much care about ivory-tower principles.
+
+I don't think LSP is "ivory-tower". It's got very practical benefits. It also
+has problems, and I agree that you don't always want to obey LSP.
+
+>... If you have
+> this problem (an added property affecting existing operations), you
+>need a mechanism to solve it.
+
+We do -- use Pre instead of Pre'Class, and then you can strengthen your
+preconditions. You pay a price for that, though -- dispatching calls can fail
+in ways that are not apparent given what's visible at the call site.
+
+That's just fine in many cases -- e.g. if there are no such dispatching calls.
+
+>...That's especially true if you are extending an existing type whose
+>specifications you can't change - I don't think there is any way to
+>preverve the Liskov property in that case. (Raising some random
+>exception rather than writing a proper precondition doesn't change
+> anything.)
+
+That (raise some arbitrary exception) is another way to defeat LSP.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 2:19 PM
+
+> But then, does it make sense to allow (class-wide) preconditions on
+> interfaces? Such things have no body!
+
+It does make sense, for the same reason it makes sense for abstract subprograms
+of abstract types. It means all the bodies in the hierarchy below this have the
+precondition. Some such bodies might not take advantage of it, but that's OK.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 2:51 PM
+
+> As Bob pointed out, most use of interfaces is with "root" types.
+
+Must've been my evil twin. But never mind...
+
+> Tucker has suggested (and I wrote up) a model where Pre'Class,
+> Post'Class, and Type_Invariant'Class preserve LSP everywhere, while
+> Pre, Post, and Type_Invariant are free-form.
+
+That's a nice summary of the model, and I think that's best, right now.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, April 1, 2011 3:03 PM
+
+> > As Bob pointed out, most use of interfaces is with "root" types.
+>
+> Must've been my evil twin. But never mind...
+
+I think I slightly mischaracterized what you previously said, which was
+something to the effect that most subprograms are inherited only from one parent
+(either an interface or some other tagged type), not multiple ones. The point
+was that the cases that cause problems are mostly corner cases. We probably
+could just make the whole bunch illegal and hardly anyone would notice.
+
+But that doesn't mean disallowing preconditions on interfaces or other broad
+strokes -- just targeted illegal cases.
+
+> > Tucker has suggested (and I wrote up) a model where Pre'Class,
+> > Post'Class, and Type_Invariant'Class preserve LSP everywhere, while
+> > Pre, Post, and Type_Invariant are free-form.
+>
+> That's a nice summary of the model, and I think that's best, right
+> now.
+
+Right. I probably ought to add a mention of this to the AI.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 3:16 PM
+
+> I think I slightly mischaracterized what you previously said, which
+> was something to the effect that most subprograms are inherited only
+> from one parent (either an interface or some other tagged type), not multiple
+> ones.
+
+Ah, yes. I remember saying that, and I still believe it.
+(And maybe my evil twin does, too.)
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Friday, April 1, 2011 3:23 PM
+
+I am sympathetic to Jean-Pierre's suggestion that Pre'Class should be forbidden
+for interfaces. Saying that you inherit from an interface is like saying you
+inherit a mortgage. What you inherit is the obligation to implement operations
+with the given signature. In a sense, that's the precondition for the use of the
+interface: these operations must be provided. Adding some predicate to these
+abstract operations does not seem to convey anything useful. Suppose you have
+an interface Serializable, that provides an operation Flatten, what precondition
+should such an operation carry? The point of the interface is to provide a
+classification mechanism for otherwise unrelated types that may land in some
+heterogenous data structure. Not only is it rare to be able to provide some
+common predicate for all implementations of the operation (when the point is
+that they will apply to objects that have no other commonality) but as this
+discussion shows, it seems hard to pin down what is the useful semantics of
+these predicates.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, April 1, 2011 3:33 PM
+
+> I am sympathetic to Jean-Pierre's suggestion that Pre'Class should be
+> forbidden for interfaces. ...
+
+I don't agree.
+
+I will be in New York on Monday, and I'll try to convince you with the help of a
+white board. And perhaps with help from Steve, who will also be in NY.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Friday, April 1, 2011 3:44 PM
+
+Looking forward....
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, April 1, 2011 3:36 PM
+
+I feel like we have given many examples of why these are useful.
+They have little or nothing to do with the underlying implementation, and
+everything to do with the abstract semantics of the operations associated with
+the interface. Open/Read/Close, Subscribe/Unsubscribe, Initialize/Add/Freeze,
+etc. I really think we will be defeating the point of having preconditions if
+we don't allow preconditions of some sort on abstract operations.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, April 1, 2011 3:41 PM
+
+Keep in mind that not having a precondition on an interface subprogram is the
+same as having a Pre'Class precondition of True on that subprogram. Since that
+is the weakest possible predicate, you are then saying that you can never have
+any class-wide predicate with an operation inherited from an interface
+(presuming you are preserving any semblance of LSP).
+
+If you are in an environment that requires LSP, that essentially means that you
+cannot use predicates with any operation that is related to an interface (since
+Pre is banned on tagged primitives in such an environment) -- or, alternatively,
+you just can't use interfaces. Neither of these seem like a good idea.
+
+While I'm surprised that anyone would require LSP, apparently that's an
+important part of DO-178C, and so I think LSP has to be an important part of
+whatever solution we use.
+
+Keep in mind that there is always an easy solution to keeping class-wide
+contract aspects LSP-compliant: ensure that they are the same all the way up.
+That can be done mechanically by banning redefinitions of Pre'Class, etc. on
+overriding routines. I suspect in 90% of real uses, this is what will happen (on
+purpose or just because it is the only thing that makes sense). It's too fierce
+to require that on all users, but keep in mind that these things we are
+discussing are rare corner cases -- it doesn't matter that much how they are
+resolved.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, April 1, 2011 4:03 PM
+
+> If you are in an environment that requires LSP, that essentially means
+> that you cannot use predicates with any operation that is related to
+> an interface (since Pre is banned on tagged primitives in such an
+> environment) -- or, alternatively, you just can't use interfaces.
+> Neither of these seem like a good idea.
+
+This is not necessarily correct, you can imagine a set of preconditions defined
+by Pre aspects, with a proof that LSP is respected, in fact I expect that to be
+a fairly common situation. So don't assume that LSP will always attempt to be
+achieved by use of the automatic weakening.
+
+> While I'm surprised that anyone would require LSP, apparently that's
+> an important part of DO-178C, and so I think LSP has to be an
+> important part of whatever solution we use.
+
+I don't know why this should be surprising, enforcing LSP is a reasonable way of
+reducing the test burden for dynamic dispatching. (think about what coverage
+means in such cases).
+
+> Keep in mind that there is always an easy solution to keeping
+> class-wide contract aspects LSP-compliant: ensure that they are the
+> same all the way up. That can be done mechanically by banning
+> redefinitions of Pre'Class, etc. on overriding routines. I suspect in
+> 90% of real uses, this is what will happen (on purpose or just because
+> it is the only thing that makes sense). It's too fierce to require
+> that on all users, but keep in mind that these things we are
+> discussing are rare corner cases -- it doesn't matter that much how they are
+> resolved.
+
+I disagree with this prediction of what will happen in 90% of cases, it does not
+match my experience with previous discussions of how to deal with coverage in
+the presence of dispatching.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, April 1, 2011 4:45 PM
+
+> > If you are in an environment that requires LSP, that essentially
+> > means that you cannot use predicates with any operation that is
+> > related to an interface (since Pre is banned on tagged primitives in
+> > such an
+> > environment) -- or, alternatively, you just can't use interfaces.
+> > Neither of these seem like a good idea.
+>
+> This is not necessarily correct, you can imagine a set of
+> preconditions defined by Pre aspects, with a proof that LSP is
+> respected, in fact I expect that to be a fairly common situation. So
+> don't assume that LSP will always attempt to be achieved by use of the
+> automatic weakening.
+
+I can imagine that, but I don't see the point of working so hard. The "effective
+precondition" (that is the precondition as expressed in all ways - Pre,
+Pre'Class, subtype predicates, constraints, assertions in the body, explicit
+code in the body) always has to be the same or weaker in order for LSP to be
+preserved. If you use Pre (or assertions and other body code), you end up having
+to prove that these are weaker than for the routine being overridden. That is
+likely to be complex. OTOH, if you use Pre'Class (and ban Pre), you already know
+that the precondition is the same or weaker, so your proof burden is mostly to
+check that the body code doesn't introduce any "implicit preconditions".
+
+So while I expect that some initial efforts might use Pre, ultimately I think
+you'll see much more use of Pre'Class.
+
+****************************************************************
+
+From: Cyrille Comar
+Sent: Sunday, April 3, 2011 8:50 PM
+
+I'm jumping in this discussion without knowing exactly what is the origin of the
+issue being discussed... Sorry about that.
+
+Le 01/04/2011 23:44, Randy Brukardt a ‚crit :
+
+> I can imagine that, but I don't see the point of working so hard. The
+> "effective precondition" (that is the precondition as expressed in all
+> ways - Pre, Pre'Class, subtype predicates, constraints, assertions in the
+> body, explicit code in the body) always has to be the same or weaker
+> in order for LSP to be preserved. If you use Pre (or assertions and
+> other body code), you end up having to prove that these are weaker
+> than for the routine being overridden. That is likely to be complex.
+> OTOH, if you use Pre'Class (and ban Pre), you already know that the
+> precondition is the same or weaker, so your proof burden is mostly to
+> check that the body code doesn't introduce any "implicit preconditions".
+
+In a formal environment, you have to achieve 2 kinds of proofs:
+
+ - verify that the code of a primitive is compatible with its contract.
+ Compatibility doesn't necessarily stops to proving that Pre ==> Post can be
+ proven with the body of the routine. It can also be interesting to verify
+ that all instructions participate to the proof of the post condition and
+ thus that the post condition is not trivial or simply weaker than what it
+ should be (or the code is doing more than what it says in the post, which
+ are 2 ways of seeing the same situation)
+
+ - verify LSP
+
+by using Pre'Class you are getting the second for free (by construction) and
+will have to work more on the first. The second part of it about competeness
+becomes a real challenge.
+
+by using Pre instead, you put yourself in a better position to do the first
+analysis but you have to do the second one as well. Since the second one is
+pretty simple to do, I think we are better off using only Pre and never
+Pre'Class. That seems even more obvious for postconditions, if all the hierarchy
+of primitives have the same post'class, you will need a lot of persuasion to
+convince anyone (and even more a prover) that you need different code in the
+different overridden bodies to achieve exactly the same thing...
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, April 4, 2011 8:50 PM
+
+> by using Pre'Class you are getting the second for free (by
+> construction) and will have to work more on the first. The second part
+> of it about competeness becomes a real challenge.
+
+You lost me here. The second part is the same either way. More below.
+
+> by using Pre instead, you put yourself in a better position to do the
+> first analysis but you have to do the second one as well. Since the
+> second one is pretty simple to do, I think we are better off using
+> only Pre and never Pre'Class. That seems even more obvious for
+> postconditions, if all the hierarchy of primitives have the same
+> post'class, you will need a lot of persuasion to convince anyone (and
+> even more a prover) that you need different code in the different
+> overridden bodies to achieve exactly the same thing...
+
+Something is wrong with your thinking here; it seems like you are thinking that
+Pre'Class and Post'Class are much more limited than they actually are. I would
+expect Pre'Class to cover exactly the same ground as a set of Pre items would.
+And thus the effort to prove using one or the other is identical. And of course,
+doing one proof is easier than doing two, so I would expect Pre'Class to be
+easier than using a set of Pre items.
+
+Considering just Pre for the moment. If you cannot write the set of your Pre
+items in terms of Pre'Class, then one of two things must be true:
+ (1) The set of Pre items violates LSP. No more to be said about that.
+ (2) The set of Pre items has insufficient abstraction to be able to be
+ modeled as one or more Pre'Class items.
+This latter case shows a design problem, because it means that the predicate
+functions needed to write the Pre'Class don't exist. And that will cause
+problems at the site of dispatching calls, because there will not be a way to
+check the predicates before making calls. Users need to be able to write
+conditionals involving the preconditions:
+ if not Is_Valid (Window) then
+ Create (Window, ...);
+ end if;
+ Draw (Window, ...);
+
+Also keep in mind two additional points:
+* It's OK to add additional Pre'Class and Post'Class items later. They are
+ combined using "or" and "and" respectively to keep LSP intact. So surely there
+ is no reason that additional postconditions can't be added.
+* The function calls in Pre'Class and Post'Class will almost always be
+ dispatching calls. As such, they automatically adjust for the changes in the
+ child objects. And these don't cost extra analysis effort for analyzing
+ dispatching bodies, as the type is always known in the Pre'Class and
+ Post'Class items - so the appropriate body can be plugged in for analysis.
+
+So it seems to me that the effort for analyzing the bodies is the same either
+way, and the effort for determining whether the preconditions and postconditions
+meet LSP drops from non-zero to zero.
+
+Moreover, using Pre prevents any analysis of dispatching calls unless full
+source code is available, while using Pre'Class allows partial designs to be
+analyzed as well complete programs. That ought to allow catching errors sooner.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, April 1, 2011 4:52 PM
+
+> The wonder and curse of OOP is that it "just works" and really isn't
+> testable in a formal sense. Most of the time, you don't need to test
+> it, either, because "it works".
+>
+> But obviously you can't use that strategy in a formal verification
+> environment. I'm not surprised that OOP has been banned in such
+> environments, but I am surprised that anyone would think that there is
+> enough value to strict LSP OOP that it would be worth allowing in such
+> environments.
+
+There are people developing critical certified code using LSP for OO stuff who
+find it quite usable, and they find it much preferable to banning OOP entirely.
+So this is real experience from important users.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Saturday, April 2, 2011 8:06 AM
+
+Does DO178-C allow multiple inheritance of interfaces? This seems surprising,
+given how cautiously OOP is being introduced in the field. I very much doubt
+that there is certified code out there that uses MI, so this discussion may be
+way ahead of current practice.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, April 2, 2011 8:11 AM
+
+I don't think DO178-C goes anywhere near this level of complex detail. And I
+agree with Ed that this discussion is way ahead of current practice. I think at
+most we will see in certified applications very conservative use of single
+inheritance with very limited use of dynamic dispatching. Cyrille, what do you
+think?
+
+****************************************************************
+
+rom: Jean-Pierre Rosen
+Sent: Sunday, April 3, 2011 3:46 AM
+
+> Does DO178-C allow multiple inheritance of interfaces? This seems
+> surprising, given how cautiously OOP is being introduced
+> in the field. I very much doubt that there is certified code out
+> there that uses MI, so this discussion may be way ahead of current
+> practice.
+
+It tends to allow interfaces, but is very cautious about full MI. (TBH, I should
+recheck from the OO supplement that I don't have at hand now, but that was the
+approach of OOTiA).
+
+Don't forget that DO178C is being pushed by Java people!
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Sunday, April 3, 2011 3:51 AM
+
+> I don't think DO178-C goes anywhere near this level of complex detail.
+> And I agree with Ed that this discussion is way ahead of current
+> practice. I think at most we will see in certified applications very
+> conservative use of single inheritance with very limited use of
+> dynamic dispatching. Cyrille, what do you think?
+
+(I'm not Cyrille ;-) ).
+
+My position for the OO panel is that I doubt that application of the LSP will be
+acceptable in practice at levels A and B. That's why I'm proposing a model that
+would make pessimistic testing acceptable, precisely by limiting dispatching to
+a small set of easily recognizable places.
+
+If that turns out to be more practical than the LSP approach, that would be a
+very good point for Ada against Java and C++ !
+
+****************************************************************
+
+From: Cyrille Comar
+Sent: Sunday, April 3, 2011 8:25 AM
+
+DO-178c doesn't ban use of multiple inheritance. It just differentiate
+inheritance of interfaces and inheritance of implementation and claims the
+former is less troublesome without imposing additional activities on the latter.
+It is thought that the new LSP verification is sufficiently of a increased
+burden to limit its use.
+
+Now, concerning the use of interfaces at the highest level of DO-178c, I don't
+think it is ahead of practice by a long shot, actually I know that it is being
+used today (albeit carefully) by a customer of us who is planned to go to
+certification in the coming year. That is still DO-178B but since this standard
+is silent in that respect, DO-178c drafts will be used as a reference until it
+becomes official. I also don't imagine how the Java crowd could live without
+interfaces and the intersection of people interested by level A and Java users
+is far from empty from what I have seen at the DO-178c committee.
+
+****************************************************************
+
+From: Stephen Michell
+Sent: Saturday, April 2, 2011 3:59 PM
+
+The reason that OOP is mistrusted in the HI field is mainly because of dynamic
+dispatching. Ada's static dispatching model is supported in Spark and is being
+accepted, but for most other languages, dynamic dispatching is all that they
+have and you cannot do enough static analysis of the code to ensure that all
+possible resolutions of a dispatching call will behave safely.
+
+****************************************************************
+
+From: Cyrille Comar
+Sent: Sunday, April 3, 2011 8:37 AM
+
+The static analysis tool that I am most familiar with (and I'm not the only one
+on this list ;-)) does enough of static analysis to ensure the above, depending
+how you define "will behave safely" but it should be able to detect a case where
+a dispatching call would lend on a primitive that has too strong a precondition
+for instance. (those who know better, please correct me)
+
+Note that what you call the "Ada's static dispatching model" is considered by
+some as pretty unsafe because it violates the "simple dispatching rule" that
+guarantees that the right method is called at run-time for the right object.
+This is a pretty controversial topic and I don't want to restart a thread on
+this but wanted to mention that the opinion expressed above is not
+representative of the whole HI community.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, April 2, 2011 7:50 PM
+
+This isn't just for DO-178C.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, April 2, 2011 8:48 PM
+
+Sure, but to me, the DO-178C standard is the most convincing argument that this
+business of weakening of preconditions makes sense (to me it otherwise does NOT
+make sense!)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, April 2, 2011 9:11 PM
+
+Apparently he folks who worked on DO-178C believe in LSP. This isn't because it
+is somehow unique to safety-critical software. Rather it is because it is a
+well established approach to making sense out of OOP. The fact that they don't
+want to adopt all of the complexities of OOP doesn't somehow lessen the
+relevance of LSP to those who do want to use, for example, multiple inheritance.
+The fact that the DO-178C folks believe in OO with LSP means that many of those
+who are more adventuresome will feel the same way. If Ada drops support for
+LSP on interfaces just because DO-178C might not use interfaces, to me that is
+just plain weird. We have interfaces, whether or not DO-178C chooses to use
+them. Many of those who use interfaces will be interested in the LSP approach,
+and it would be weird to support it just for the subset that we *think* DO-178C
+folks are interested in (in fact, I have not seen anything that indicates they
+won't use interfaces).
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, April 2, 2011 9:40 PM
+
+I think you are misunderstanding the motivations here somewhat.
+
+The issue in DO-178C is coverage testing which conceptually involves testing
+every possible flow control path to make sure it is taken.
+
+For dynamic dispatching this would mean making sure that for every call and
+every method that corresponds, the path is indeed taken.
+
+This is impractical for two reasons.
+
+a) too many paths
+
+b) not all of them are possible anyway
+
+LSP is seen as a means to satisfactorily allow more limited testing, the idea
+being that if one path is taken, then since in some sense all possible paths are
+the "same", this is good enough.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Sunday, April 3, 2011 3:44 AM
+
+Let's be clear:
+
+1) LSP is not automatic, and it is possible to give very convincing examples of
+ violations of the LSP. IF a program obeys by the LSP, some interesting
+ properties can be proven (like not requiring pessimistic testing for DO178C).
+ Where the language can help is by a) making easier to show that LSP is being
+ obeyed, and b) raising an exception if it is assumed and not obeyed. The
+ issue is NOT on forcing LSP on every program.
+
+2) If the caller has a certain view of an object, he is bound by that view, and
+ nothing else. If I have an object that belongs to A'Class, and the actual is
+ a B (derived from A), my part of the contract is only in fulfilling the
+ preconditions for A - hence the "weakening" semantics of preconditions.
+ Everybody (I hope!) agrees with that. But see below for interfaces.
+
+3) There are two ways of enforcing the contract: statically (automatic "oring"
+ of preconditions), or dynamically (raise an exception in case of precondition
+ failure).
+
+Now, the whole issue is what to do with interfaces. Automatic "oring" simply
+does not work, as pointed out repeatedly. Why? because implementing an interface
+is not the same thing as inheriting. Inheritance happens serially between
+classes that belong to a common family, organized by increasing specialization.
+Implementing an interface is done by classes that have no relationship
+whatsoever, and all implementations of interfaces of a given class happen in
+parallel. (Randy - and many people - view interfaces as a kind of MI, I don't.
+That's part of the disagreement).
+
+What I'm proposing is automatic "oring" of preconditions for derivation, but not
+between the various progenitors. If you call an operation through a view of one
+progenitor, other preconditions (whether specific or class-wide) are checked at
+run-time. In other words, this would have the effect that preconditions from a
+serial branch are "ored" (statically), and preconditions from parallel branches
+are "anded" (dynamically). Might make more sense if stated this way...
+
+As far as the LSP is concerned: it is automatically enforced at compile time for
+derivation (serial branches), and dynamically enforced between parallel
+branches. IOW, if you use an operation that has its own preconditions to
+implement an operation from an interface, it is your responsability to make sure
+that you don't violate LSP (possibly by "oring" the preconditions from the
+interface into the implementing routine yourself).
+
+Note that with this model, I'm now moving in favor of allowing preconditions on
+interfaces, otherwise an interface without preconditions could be implemented
+only by a procedure without preconditions (if you want the LSP, of course). In a
+sense, an interface has to balance between very strong preconditions (making
+implementation easier, since it leaves much space for weakening), an weak
+preconditions (more user-friendly, more burden for the implementation).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, April 3, 2011 10:07 AM
+
+I don't think there is always such a stark contrast between interfaces and
+non-interface types. I suspect that as Ada 2005 becomes more widely used, we
+will see some projects move what were abstract tagged types into being
+interfaces, and some projects that initially use interfaces for everything move
+some of the interfaces back to being "normal" tagged types, just so they can
+provide more flexible "default" implementations. Or we will see what happens in
+Java, where many interfaces have "default" non-interface types, which implement
+the interface, and can be used as a place to provide more complex defaults.
+
+So I think we would be interfering with natural evolution if we set up
+significantly different rules between "normal" tagged types and interfaces.
+Also, we have in several places made certain that whether a particular interface
+is considered the "parent" type or one of the "progenitor" types has no net
+effect on semantics. It affects the vocabulary, but that is about all. We should
+be careful to preserve that.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, April 3, 2011 10:31 AM
+
+An interface is conceptually the same thing as an abstract type with
+all-abstract ops. Interfaces are a bit more flexible, that's all.
+
+Therefore, it makes no sense to me to place arbitrary restrictions on
+interfaces, different from abstract types.
+
+It also makes no sense to make them behave differently in some subtle way.
+
+****************************************************************
+
+From: Dan Eilers
+Sent: Sunday, April 3, 2011 11:19 AM
+
+In this example, T1a is an abstract type, and T1b is a limited interface.
+So you would not expect them to behave differently in some subtle way.
+But they behave differently with regard to inheritance of limitedness, causing
+T3a derived from T1a to be legal, and T3b derived from T1b to be illegal.
+
+
+package P is
+
+ type T1a is abstract tagged limited null record;
+ type T1b is limited interface;
+
+ type T2 is limited null record;
+
+ type T3a is new T1a with record
+ a1: T2; -- OK
+ end record;
+
+ type T3b is new T1b with record
+ a2: T2; -- ERROR:
+ end record;
+end P;
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, April 3, 2011 12:03 PM
+
+Good point, but the alternative (as explained in AARM 7.5(6.c)) was that order
+mattered when there was one parent and one progenitor and both were interfaces.
+We went with the rule where order didn't matter if both orders were legal, in
+"type A is new B and C with ...".
+
+But you are right, if components are being inherited, the rules on limitness
+inheritance are different. We could have conceivably said that from a visibly
+limited null record type, limitness was not inherited.
+
+So this does give an incentive to change a null abstract tagged limited
+non-interface type into being a limited interface type. Which is probably
+another reason not to have different rules in other regards, so you don't end up
+in a nasty either/or -- such as, "either you can make it a non-interface type,
+in which case limitness is inherited, or you can make it an interface type, in
+which case you have different limitations."
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, April 3, 2011 11:29 AM
+
+> In this example, T1a is an abstract type, and T1b is a limited interface.
+> So you would not expect them to behave differently in some subtle way.
+> But they behave differently with regard to inheritance of limitedness,
+> causing T3a derived from T1a to be legal, and T3b derived from T1b to
+> be illegal.
+
+When I said "behave ... subtle", I was talking about run-time behavior.
+Subtle compile-time rules are much less harmful.
+
+You're right that T3b is illegal, and my previous paragraph ("Therefore, ...")
+is about compile-time restrictions. But there's no real restriction here --
+just add "limited". That's subtle, I suppose, but GNAT tells you exactly what
+to do.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, April 4, 2011 7:35 AM
+
+> I don't think there is always such a stark contrast between interfaces
+> and non-interface types. I suspect that as Ada 2005 becomes more
+> widely used, we will see some projects move what were abstract tagged
+> types into being interfaces, and some projects that initially use
+> interfaces for everything move some of the interfaces back to being
+> "normal" tagged types, just so they can provide more flexible
+> "default" implementations.
+That's possible, but I don't think it changes anything to the discussion
+
+> Or we will see what happens in Java, where many interfaces have
+> "default" non-interface types, which implement the interface, and can
+> be used as a place to provide more complex defaults.
+... IMHO, an horrible Java habit.
+
+> So I think we would be interfering with natural evolution if we set up
+> significantly different rules between "normal" tagged types and
+> interfaces.
+> Also, we have in several places made certain that whether a particular
+> interface is considered the "parent" type or one of the "progenitor"
+> types has no net effect on semantics.
+> It affects the vocabulary, but that is about all.
+> We should be careful to preserve that.
+
+The different rules are not between tagged types and interfaces. They are
+between derivation and multiple progenitors.
+
+I may not have made myself clear, so here it is what I'm suggesting:
+- If B derives from A and both have (class-wide) preconditions, the effective
+ precondition is the "or" of both (I think this is accepted)
+- If a tagged type C has progenitors A and B with (class-wide) preconditions on
+ operation O, the effective precondition for O is the "and" of both.
+
+This comes from the following requirements:
+1) If the user gets an object as an A'Class, the only contract on its part is in
+ fulfilling the class-wide preconditions for A.
+2) When the body is called (which in general is not an A), all applicable
+ preconditions (wheter class-wide or specific) are met, or Assertion_Error is
+ raised.
+
+Can we agree on these requirements?
+Note that to obey LSP, a class needs to ensure that 1) implies 2).
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, April 4, 2011 7:37 AM
+
+> An interface is conceptually the same thing as an abstract type with
+> all-abstract ops. Interfaces are a bit more flexible, that's all.
+
+Yes, from an implementation point of view. The same way that all this stuff
+about OOP is no more than a glorified table of pointers to subprograms. And ifs
+are just gotos in disguise.
+
+ From a methodological point of view, there are differences, though.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, April 4, 2011 8:09 AM
+
+>I may not have made myself clear, so here it is what I'm suggesting:
+>- If B derives from A and both have (class-wide) preconditions, the effective
+> precondition is the "or" of both (I think this is accepted)
+>- If a tagged type C has progenitors A and B with (class-wide) preconditions on
+> operation O, the effective precondition for O is the "and" of both.
+
+>This comes from the following requirements:
+>1) If the user gets an object as an A'Class, the only contract on its part is in
+> fulfilling the class-wide preconditions for A.
+>2) When the body is called (which in general is not an A), all applicable
+> preconditions (wheter class-wide or specific) are met, or Assertion_Error is
+> raised.
+
+That's a very intuitive description of the desired rule, I think it's the right
+formulation.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, April 4, 2011 12:13 PM
+
+After further discussion ... when you you say "
+
+- If a tagged type C has progenitors A and B with (class-wide) preconditions on
+ operation O, the effective precondition for O is the "and" of both"
+
+I understand that you want the conjunction for INVARIANTS of the type (f it's
+an A and a B it better have the characteristics of both). But for the
+preconditions of a given operation this would mean that the caller on a
+dispatching call doesn't see all the applicable requirements, and gets an
+Assertion_Error in spite of having satisfied the precondition he knows about.
+This can't possibly be what you want.
+
+Leaving aside multiple progenitors, the common case is a type that inherits from
+one interface and from one concrete type that provides an implementation for
+the operations of the interface. The precondition is a consistency relation
+between abstract operations: there is an abstract operation AO, an abstract
+predicate AP, and we state that AO can be called if AP is true. Given the
+corresponding operations of the concrete type, CO and CP, we want the same
+relationship between them: if CP obtains, CO is callable. There is no issue of
+and'ing or or'ing here. A dispatching call verifies AP (which is itself
+dispatching a dispatches to CP). It's up to the programmer to verify that the
+abstract and concrete operations are in the same relationship to each other.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, April 4, 2011 3:48 PM
+
+> I understand that you want the conjunction for INVARIANTS of the type
+> (f it's an A and a B it better have the characteristics of both). But
+> for the preconditions of a given operation this would mean that the
+> caller on a dispatching call doesn't see all the applicable
+> requirements, and gets an Assertion_Error in spite of having satisfied
+> the precondition he knows about. This can't possibly be what you want.
+Yes it is.
+
+If this happens, it means that the implementation of the interface does not meet the LSP. I don't think it is our business to *require* the LSP everywhere - there are too many examples where the LSP does not work.
+
+I'm just saying that it's the implementor's business to make sure that the LSP is met (if desired) - possibly by manually "oring" the precondition from the interface into its own preconditions.
+
+Note that this is exactly similar to what happens if a specific precondition is stronger than the class-wide precondition.
+
+> Leaving aside multiple progenitors, the common case is a type that
+> inherits from one interface and from one concrete type that provides
+> an implementation for the operations of the interface. The
+> precondition is a consistency relation between abstract operations:
+> there is an abstract operation AO, an abstract predicate AP, and we
+> state that AO can be called if AP is true. Given the corresponding
+> operations of the concrete type, CO and CP, we want the same
+> relationship between
+> them: if CP obtains, CO is callable. There is no issue of and'ing or
+> or'ing here. A dispatching call verifies AP (which is itself
+> dispatching a dispatches to CP). It's up to the programmer to verify
+> that the abstract and concrete operations are in the same relationship
+> to each other.
+
+I don't get you here, if you check AP, you check AP, not CP!
+
+Once again, I think there is a fundamental difference between interfaces and
+inheritance. IMHO, an interface is written by the user of the interface. Take a
+"serializable" interface for example. It basically says: "if you give me a type
+with a Put operation, I can save it to a disk". A precondition says: "I promise
+never to call Put on a closed file" (and therefore you don't need to check it
+yourself).
+
+If the implementer has extra conditions, and these are not met, it raises an
+exception. That's what happens if the user pulls out the diskette - sorry the
+USB key ;-) - while the Put is in progress.
+
+If you want to use LSP proofs, you have to prove that no implementation has
+stronger conditions than what is promised by the interface's preconditions.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Monday, April 4, 2011 6:54 PM
+
+You can't check AP, it's abstract! The call to AP in the precondition is a
+dispatching call, that executes CP of course.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, April 5, 2011 3:13 AM
+
+I'm completely confused here. A (class-wide) precondition is a boolean
+expression that follows "with Pre'class =>". How can it be abstract?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, April 5, 2011 6:25 AM
+
+The functions it calls can be abstract.
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Tuesday, April 5, 2011 7:36 AM
+
+Because it can only be a call to a subprogram, you have no components with which
+to write an expression. That subprogram is itself a primitive of the interface,
+and the expression will be a dispatching call.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, April 5, 2011 1:24 PM
+
+Huh? Are there any special visibility rule that would prevent me from writing an
+expression involving only global variables? Or functions from some other
+package? or a combination of functions (primitive or not)?
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Tuesday, April 5, 2011 1:34 PM
+
+Of course not, but I suspect that this will be the unusual case. All the
+examples used so far assume that some primitive operations are accessors and
+modifiers, and others are predicates that control the legality of the former. I
+have not seen credible examples involving existing data structures or global
+entities.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, April 5, 2011 1:36 AM
+
+A "good" precondition will depend on the values of the parameters of the
+operation, that necessarily involves other primitives of an interface type
+(there cannot be anything else that takes the interface type).
+
+There isn't a language rule against writing a junk precondition (it's too hard
+to define), but there is no reason to care what happens for such things. It's
+irrelevant.
+
+I don't understand why you care anyway about a concept that necessarily violates
+LSP. (See my other message.) Class-wide preconditions are intended solely for
+uses where LSP is preserved. As I noted in my other message, I know think these
+should be illegal (unless there is a brand-new body involved). Please explain
+why we should ingrain LSP violations in the language (I think that would be
+horrible for uses where LSP is required, especially as it would be implicit).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, April 4, 2011 9:49 PM
+
+...
+> The different rules are not between tagged types and interfaces. They
+> are between derivation and multiple progenitors.
+>
+> I may not have made myself clear, so here it is what I'm suggesting:
+> - If B derives from A and both have (class-wide) preconditions, the
+> effective precondition is the "or" of both (I think this is accepted)
+> - If a tagged type C has progenitors A and B with
+> (class-wide) preconditions on operation O, the effective precondition
+> for O is the "and" of both.
+>
+> This comes from the following requirements:
+> 1) If the user gets an object as an A'Class, the only contract on its
+> part is in fulfilling the class-wide preconditions for A.
+> 2) When the body is called (which in general is not an A), all
+> applicable preconditions (wheter class-wide or specific) are met, or
+> Assertion_Error is raised.
+>
+> Can we agree on these requirements?
+
+No. I think class-wide preconditions are a different beast that never needs
+checking in the body.
+
+> Note that to obey LSP, a class needs to ensure that 1) implies 2).
+
+Right, and that is impossible given the rules that you suggest. That's why it is
+unacceptable.
+
+As soon as you combine two preconditions A and B with "and", you've violated LSP
+(unless one is "True" or A = B for all objects). Moreover, you can't fix it by
+adding a new Pre condition: (A and B) and (A or B) = (A and B). So if we adopt
+this as the rule for multiple inheritance, you've killed LSP for all time on
+interfaces. That's a non-starter.
+
+Besides, I think you are focusing on the wrong thing. When you say that
+interfaces "are not about multiple inheritance", I tend to agree -- but the
+troublesome cases are all multiple inheritance cases. I don't much care about
+the cases that are not problems! (So long as we don't break them.) More detail
+below.
+
+===
+
+The discussion this weekend has given me more indication that preserving LSP is
+very important. Thus I think it is critical that the class-wide things
+(Pre'Class, Post'Class, and Type_Invariant'Class) never violate LSP on their
+own. (Obviously, the body of a routine can violate LSP, the language cannot do
+anything to ensure that.) If someone wants to violate LSP, they have to use Pre,
+Post, etc. (Or just randomly raise exceptions in the body!)
+
+It should be noted that having both a Pre'Class and a Pre for a routine
+automatically violates LSP. (You can use *only* Pre and still have LSP, but
+never both [unless one is trivial].) Thus I'm not even going to consider Pre
+when discussing this; it's separate from any discussion of preconditions and
+LSP.
+
+Anyway, I think that we need to take a more serious look at the rules to ensure
+that we are not doing something that violates LSP for Pre'Class. As such, I have
+a new proposal below (well, it's old, but it never was written up).
+
+But first to motivate my suggestion:
+
+The first thing to remember is that having multiple direct ancestors doesn't
+really matter here. It is the inheritance of the subprograms that matters, not
+the parent and progenitor types. If only one of the ancestor types has a
+particular operation, then the Pre'Class only comes from that ancestor. That is
+the normal single inheritance case. This is by far the most common case in
+practice (as Bob pointed out last week).
+
+Now, assume we do have two operations, with class-wide preconditions A (for type
+A_T [any tagged type]) and B (for type B_T [an interface]). (The natural
+extension occurs when there are more than two, so we'll only talk about two). So
+when we inherit these, we get a precondition of (A or B). That's the only
+precondition that would not violate LSP, since dispatching calls on type A_T
+will check only A, and dispatching calls on type B_T will check only B.
+
+Thus, the body will see a precondition of A or B. If the body is provided by
+overriding, LSP can be preserved by writing the body properly. That will
+probably require avoiding calling the parent operation (if A_T is concrete), as
+it will have a stronger precondition A. Thus, "writing the body properly" may
+not be easy, but it is possible, and since we've already stipulated that the
+language cannot do anything to help here, that's pretty much the end of the
+discussion.
+
+However, if the operation is inherited, then there is trouble. This is
+effectively calling the parent operation with a precondition of A, but the
+operations precondition is A or B. This is especially bad if the operation is
+called through type B_T'Class, as in that case the only precondition check will
+be B. And checking A necessarily violates LSP.
+
+Indeed, inheritance of concrete routines always will violate LSP if there is
+more than one direct ancestor operation. This appears to be fundamental to me,
+it is not something that we can avoid by tweaking the rules. There is no way to
+avoid the problem that there are more preconditions on such a dispatching call
+than the caller knows about -- which is the definition of LSP.
+
+Note that there is a similar (but much less serious) problem with
+postconditions. In this case, there are multiple postconditions that need to be
+checked; the inherited routine does not know about all of them, and given that
+compilers are probably going to generate postconditions inside of the subprogram
+bodies, the additional ones will have to be added somehow.
+
+Also note that Tucker's problem with renaming overridings is essentially this
+same problem: in that case, the inherited preconditions may have no relationship
+to the preconditions of the renamed routine.
+
+=================
+
+Given that inheritance of subprograms with multiple direct ancestors always
+violates LSP, I no longer think that the language should automatically construct
+such subprograms (as proposed in the current draft of AI05-0247-1). If you're
+going to do something that violates LSP, you ought to have it explicitly in the
+program source code where tools can see it. It's nasty to make proof tools try
+to figure out the Ada inheritance rules!
+
+Therefore, I am now leaning to requiring overriding for such inheritance. The
+only exception would be for routines that have no Pre'Class, Post'Class, or
+Type_Invariant'Class that apply (for the first two, the expressions would be
+"True"). We could do better than that, but it would require a messy new concept
+(two preconditions for different types can never be fully conformant, so we'd
+need a new version of conformance that took type differences and the associated
+function differences into account). This is not likely to be that common, as
+multiple inheritance of an operation is not that common.
+
+In this multiple inheritance case, if the user can write an LSP-compliant body,
+they can do so, and there is no problem. If they have to violate LSP, they can
+write a body doing that, too. But we're not going to do that automatically for
+them.
+
+[The renames case then has to be just illegal. Again, a full body would work in
+place of the renames, so this is no significant loss.]
+
+==================
+
+I'd be happy to write up a new version of AI05-0247-1 to this end, but:
+(1) I'd be violating the promise of no new wording I made on Friday;
+(2) I'm not certain that enough people agree with this approach to make it
+ worthwhile.
+
+I do note that this point is critical to the success of Ada 2012.
+Preconditions are central to the new features in Ada, and we cannot get them
+wrong (or omitted). The only alternative IMHO is to abandon all hope and
+completely drop Pre'Class, et. al., especially as Cyrille says that he thinks it
+would be easier not to use them. But I think that it permanently denying
+dispatching call-site analysis to compilers or other tools without full source
+capability -- not what I signed up for.
+
+So I would like to see if there is any way to get a resolution of this on
+Thursday, otherwise, Ada 2012 will be delayed for a year...
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Wednesday, April 6, 2011 3:03 AM
+
+> Of course not, but I suspect that this will be the unusual case. All
+> the examples used so far assume that some primitive operations are
+> accessors and modifiers, and others are predicates that control the
+> legality of the former. I have not seen credible examples involving
+> existing data structures or global entities.
+
+External protection against concurrent access: the caller must hold some
+semaphore.
+
+There are also often conditions involving the non-controlling parameters
+
+In any case, we can't assume that "it can only be a call to a subprogram [...
+which] is itself a primitive of the interface"
+
+****************************************************************
Questions? Ask the ACAA Technical Agent