CVS difference for ai05s/ai05-0247-1.txt

--- ai05s/ai05-0247-1.txt	2011/05/12 23:03:01	1.10
+++ ai05s/ai05-0247-1.txt	2011/06/03 02:42:13	1.11
@@ -1,7 +1,8 @@
-!standard 6.1.1(0)                                    11-05-12  AI05-0247-1/09
+!standard 6.1.1(0)                                    11-06-02  AI05-0247-1/10
 !standard 7.3.2(0)
 !reference AI05-0145-2
 !class Amendment 11-03-21
+!status ARG Approved (by Letter Ballot) 8-0-3  11-05-16
 !status work item 11-03-21
 !status received 11-03-17
 !priority High
@@ -175,7 +176,7 @@
 Pack3.P3 is weaker (Is_Green(Obj) or Is_Valid(Obj)). Thus we end up checking the
 precondition of the actual body in this case, not the weaker precondition of the
 body Pack3.P3. Indeed, the effect is to *and* the preconditions when called on
-an object of type T2'Class (since we also have to check the precondition
+an object of type I2'Class (since we also have to check the precondition
 expected by the interface dispatching call). OTOH, a dispatching call using an
 object of T1'Class does not need to check Is_Green at all.
 
@@ -293,7 +294,7 @@
   subprogram. [Redundant: Only the Pre'Class and Post'Class aspects may
   be specified for such a subprogram.]
 
-  If a type has a inherited subprogram P implicitly declared, the corresponding
+  If a type has an inherited subprogram P implicitly declared, the corresponding
   primitive subprogram of the parent or progentitor is neither null nor
   abstract, a homograph (see 8.3) of P is declared and inherited from an
   ancestor T2 that is different from the ancestor T1 from which P is inherited,
@@ -439,7 +440,7 @@
 
           Dynamic Semantics
 
-  If the Assertion_Policy (see 11.4.2) in effect at the point of a subprogram
+  If the assertion policy (see 11.4.2) 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:
@@ -467,7 +468,7 @@
   are performed prior to checking whether the entry is open.
 
 
-  If the Assertion_Policy in effect at the point of a subprogram or entry
+  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
@@ -553,10 +554,10 @@
     for 'Access values.
     End AARM Implementation Note.
 
-  If the Assertion_Policy in effect at the point of a
+  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
+  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.
@@ -577,11 +578,14 @@
 
 Move 13.3.3 [from AI05-0146-1] to clause 7.3.2.
 
+In 7.3.2(8/3), change "Assertion_Policy" to "assertion policy" (as that is the
+term defined in 11.4.2).
+
 Modify 7.3.2(18/3):
 
 The invariant checks performed on a call are determined by the subprogram or entry
 actually invoked, whether directly, as part of a dispatching call, or as part of a
-call through an access-to-subprogram value.  For the purposes of
+call through an access-to-subprogram value. For the purposes of
 these checks, if the subprogram actually invoked is primitive for some type T and
 is inherited from some other type, the checks needed are determined as if the
 body of the of the entity is declared directly as a primitive of type T;
@@ -591,12 +595,12 @@
     AARM Ramification: We use the "for these purposes" part of the rule to include
     additional Type_Invariant'Class checks from those that apply to the original
     subprogram. This may happen if the operation is inherited from both a parent
-    and a progenitor, nd both the parent operation and progenitor operation have
+    and a progenitor, and both the parent operation and progenitor operation have
     defined a Type_Invariant'Class.
 
     For inherited concrete routines, we require the original Type_Invariant to be
     evaluated as well as the inherited Type_Invariant'Classes and the current type's
-    Typee_Invariant in order that the semantics of an explicitly defined wrapper that
+    Type_Invariant in order that the semantics of an explicitly defined wrapper that
     does nothing but call the original routine is the same as that of an inherited
     routine.
     End AARM Ramification.
@@ -657,7 +661,8 @@
      procedure Foo (Param : Int2) is null
         with Pre'Class => Is_Good (Param);
 
-     type Int3 is Int1 and Int2;
+     type Int3 is Int1 and Int2 with null record;
+     function Is_Good (P : Int3) return Boolean;
 
 6.3.1(21) requires that each direct_name in an expression have to denote the same
 declaration. But in this example, neither Param nor Is_Good denote the same
@@ -671,7 +676,7 @@
 specifications (to clause 6.1.1) as these are strongly associated with these. It
 doesn't make sense for this section to be defined in chapter 13, especially
 with the Inline and No_Return aspects defined in Chapter 6. These are arguably
-more important.
+more important than those, so we don't want to bury them.
 
 Similarly, we move type invariants to clause 7.3.2, directly after private types
 to which they apply.
@@ -8496,5 +8501,38 @@
 
 Tucker didn't vote yet, but since we have a landslide, I'm declaring a winner,
 putting it into the AI, and moving on to the letter ballot.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, May 1, 2011 11:36 AM
+
+I have been out of town, at the Penn Relays (a truly amazing track meet -- 45,000
+people in the stands screaming at the top of their lungs for people running track!?).
+
+I thought we could convert chapter 13 into a general chapter on "Program Annotation"
+but that didn't seem to garner much interest.  Failing that, I am happy to follow
+along with the general consensus on where to locate pre/postconditions.
+
+****************************************************************
+
+From: Brad Moore
+Sent: Sunday, May 15, 2011  2:52 PM
+
+[Appropriate part of a large message - Editor.]
+
+> AI05-0247-1/09  Preconditions, Postconditions, multiple inheritance, 
+> and dispatching calls
+>     [Changes as discussed during the phone meeting: Added rules to require overriding
+>     for inherited routines which would either violate LSP or have unenforced preconditions;
+>     changed rules for calling inherited subprograms such that there is always an implicit
+>     body involved (this has appropriate postconditions and invariants); simplified 3.9.2(20.3/3)
+>     based on the previous.]
+>     Approve __X____ Disapprove ______ Abstain _______
+
+Editorial Comment: In the problem section, T2'Class should be I2'Class.
+
+Editorial Comment: Legality Rules, 2nd Para. "If a type has a inherited" 
+=> "If a type has an inheritied"
 
 ****************************************************************