CVS difference for ai12s/ai12-0131-1.txt

--- ai12s/ai12-0131-1.txt	2014/10/10 00:34:25	1.1
+++ ai12s/ai12-0131-1.txt	2014/11/14 02:30:41	1.2
@@ -1,6 +1,8 @@
 !standard 6.1.1(17/3)                                14-10-09  AI05-0131-1/01
 !standard 6.1.1(18/3)
 !class binding interpretation 14-10-09
+!status Corrigendum 2015 14-11-13
+!status ARG Approved 7-0-1  14-10-18
 !status work item 14-10-09
 !status received 14-08-01
 !priority Medium
@@ -10,7 +12,7 @@
 !summary
 
 If the initial definition of a primitive subprogram of a tagged type does
-not specify Pre'Class, the corrsponding subprograms of descendant types
+not specify Pre'Class, the corresponding subprograms of descendant types
 inherit a class-wide precondition of True. 
 
 !question
@@ -37,7 +39,7 @@
 
 For (3), the specified Pre'Class is evaluated; 6.1.1(18/3) says that no
 precondition is inherited (since none are specified on (1)). So the
-precondition that is evaluared is Is_OK(S_Obj).
+precondition that is evaluated is Is_OK(S_Obj).
 
 For (4), there is no specified precondition (6.1.1(38/3) says that we don't
 care about the class-wide preconditions of the actual body, only the subprogram
@@ -56,7 +58,7 @@
 
 !wording
 
-[Optional] Add after 6.1.1(17/3):
+Add after 6.1.1(17/3):
 
    Pre'Class shall not be specified for an overriding primitive
    subprogram of a tagged type T unless Pre'Class is specified
@@ -73,31 +75,39 @@
 instance, if the parent subprogram has explicitly specified a
 precondition of True).
 
+    In addition to the places where Legality Rules normally apply (see 12.3),
+    these rules also apply in the private part of an instance of a generic
+    unit.
+
+[Editor's note: It appears that instance rechecking also is needed for
+6.1.1(16/3) and 6.1.1(17/3), thus the plural form of the boilerplate
+was used.]
+
 Revise 6.1.1(18/3) as follows:
 
    If a Pre'Class or Post'Class aspect is specified for a primitive
    subprogram of a tagged type T, {or such an aspect defaults to
-   True when no other Pre'Class or Post'Class applies to the subprogram},
-   then the associated expression also applies to the
+   True,} then the associated expression also applies to the
    corresponding primitive subprogram of each descendant of T. 
 
-[Editor's note: Tucker included Post'Class in this wording in his
-version that appears in AI12-0113-1. I've kept that, although it is
-irrelevant -- we could just define this for Pre'Class. I also expanded
-his wording to make it clear that the new condition only applies when
-there is nothing specified for Pre'Class, we don't want overriding
-routines to have to re-specify Pre'Class just to prevent the implicit
-True from counterfeiting the inherited precondition.]
+AARM Ramification: A Pre'Class defaults to True only if no class-wide
+preconditions are inherited for the subprogram. The same is true for
+Post'Class.
+
+AARM Reason: We have to inherit precondition expressions that
+default to True, so that later overridings don't strengthen the
+precondition (a violation of LSP). We do the same for postconditions
+for consistency.
 
 !discussion
 
 Note that specifying a class-wide precondition on (2) [the overriding
-subprogram] is strengthening the the precondition, a violation of
-the Liskov Substituability Principle [LSP]. But Pre'Class is intended to
-directly model LSP.
+subprogram] is strengthening the precondition, a violation of the Liskov
+Substitutability Principle [LSP]. But Pre'Class is intended to directly model
+LSP.
 
-Thus we say that a overriding a subprogram that has no Pre'Class specified
-causes the new subprogram to inherit a Pre'Class of True.
+Thus we say that overriding a subprogram that has no Pre'Class specified
+for any ancestor causes the new subprogram to inherit a Pre'Class of True.
 
 Note that this only applies to "root" subprograms that don't have Pre'Class;
 overriding subprograms that don't have Pre'Class just inherit whatever
@@ -106,33 +116,55 @@
 precondition, which is certainly not what we want.
 
 ---
-
-The change to 6.1.1(18/3) is formally an inconsistency, as it will weaken the
-precondition that applies to statically bound calls (like call (3) in the
-question). This might be a problem if the body of the called subprogram
-(P in the example) assumes that the precondition is checked.
-
-As such, we propose a Legality Rule to effectively change this inconsistency
-into an illegality. Any such Pre'Class would have no effect (it would be
-"counterfeited") and would be dangerously misleading to readers. This
-Legality Rule is optional in that we don't need it to have well-defined
-semantics.
 
-That would make this Legality Rule a candidate for being a suppressible
-error (see AI12-0092-1), should that idea ever make it into the Standard.
+The change to 6.1.1(18/3) is formally an inconsistency, as it will weaken
+(in fact, eliminate) the class-wide precondition that applies to statically
+bound calls (like call (3) in the question). This might be a problem if the
+body of the called subprogram (P in the example) assumes that the class-wide
+precondition is checked, and there were no dispatching calls in the program
+(which are already unchecked).
+
+As such, we defined a Legality Rule to effectively change this inconsistency
+into an illegality (and incompatibility with the original definition of Ada 2012).
+Any such Pre'Class would have no effect (it would be "counterfeited") and
+would be dangerously misleading to readers.
+
+!corrigendum 6.1.1(17/3)
+
+@dinsa
+If a renaming of a subprogram or entry @i<S1> overrides an inherited subprogram
+@i<S2>, then the overriding is illegal unless each class-wide precondition
+expression that applies to @i<S1> fully conforms to some class-wide
+precondition expression that applies to @i<S2> and each class-wide precondition
+expression that applies to @i<S2> fully conforms to some class-wide
+precondition expression that applies to @i<S1>.
+@dinss
+Pre'Class shall not be specified for an overriding primitive
+subprogram of a tagged type @i<T> unless Pre'Class is specified
+for the corresponding primitive subprogram of some ancestor of @i<T>.
+
+In addition to the places where Legality Rules normally apply (see 12.3),
+these rules also apply in the private part of an instance of a generic unit.
+
+!corrigendum 6.1.1(18/3)
+
+@drepl
+If a Pre'Class or Post'Class aspect is specified for a primitive subprogram
+of a tagged type @i<T>, then the associated expression also applies to the
+corresponding primitive subprogram of each descendant of @i<T>.
+@dby
+If a Pre'Class or Post'Class aspect is specified for a primitive subprogram
+of a tagged type @i<T>, or such an aspect defaults to
+True, then the associated expression also applies to the
+corresponding primitive subprogram of each descendant of @i<T>.
 
 !ASIS
 
 No ASIS effect.
 
 !ACATS test
-
-If we include the Legality Rule option, then an ACATS B-test should be
-constructed to test that rule. If we don't include the Legality Rule, we
-need an ACATS C-Test to verify that Pre'Class is inherited as
-True when not specified for the parent, even if Pre'Class is specified
-on the child subprogram.
 
+An ACATS B-test should be constructed to test the new Legality Rule.
 
 !appendix