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

--- ai12s/ai12-0236-1.txt	2019/01/11 08:27:40	1.6
+++ ai12s/ai12-0236-1.txt	2019/01/16 00:47:58	1.7
@@ -1,10 +1,14 @@
-!standard 3.9.2(3)                                    18-12-06  AI12-0236-1/04
+!standard 3.9.2(3)                                    19-01-15  AI12-0236-1/05
 !standard 3.10.2(9.1/3)
 !standard 3.10.2(32.2/3)
+!standard 4.3.2(5.4/3)
+!standard 4.3.3(15.1/3)
+!standard 6.2(10/4)
 !standard 6.9(0)
-!standard 7.6.1(3/2)
 !standard 8.1(3)
 !class Amendment 17-09-06
+!status Amendment 1-2012 19-01-15
+!status ARG Approved 8-1-3  19-01-14
 !status work item 17-09-06
 !status received 17-06-21
 !priority Low
@@ -27,7 +31,7 @@
 This often leads to repeating the same expression several times within
 contracts.
 
-Take the following subprogram and its post-condition into consideration:
+Take the following subprogram and its postcondition into consideration:
 
    procedure Fgetc (Stream : File_Descr; Result : out Int) with
      Post =>
@@ -95,6 +99,21 @@
 elaborated in order, and then the *body_*expression is evaluated. The
 value of the declare_expression is that of the *body_*expression.
 
+Examples
+
+The postcondition for Ada.Containers.Vectors."&" (see A.18.2) could have
+been written:
+
+   with Post =>
+      (declare
+         Result renames Vectors."&"'Result;
+         Length : constant Count_Type := Left.Length + Right.Length;
+       begin
+         Result.Length = Length and then
+         not Tampering_With_Elements_Prohibited (Result) and then
+         not Tampering_With_Cursors_Prohibited (Result) and then
+         Result.Capacity >= Length)
+
 [End of new 6.9]
 
 Add after the penultimate sentence of 3.9.2(3):
@@ -111,13 +130,25 @@
 
    * a declare_expression (see 6.9); or
 
-Add after 4.3.2(5.4), in the rule for extension aggregates:
+Add after 4.3.2(5.4/3), in the rule for extension aggregates:
 
    * a declare_expression whose *body*_expression would violate this
      rule.
+
+   [Editor's note: We have to add a semicolon and "nor" to the previous
+   bullet, to match the others in this set.]
 
-Add to the end of 6.2(10):
+Adding after 4.3.3(15.1/3): (this allows "others" in *body_*expressions)
+
+        For a declare_expression, the applicable index constraint for
+        the *body*_expression is that, if any, defined for the
+        declare_expression.
 
+  [Editor's note: We have to change the period to a semicolon on the previous
+   bullet.]
+
+Add to the end of 6.2(10/4):
+
     For a declare_expression, this object is the one associated with the
     *body*_expression.
 
@@ -140,13 +171,6 @@
 The restriction to nonlimited types is to avoid implementation
 difficulties related to build-in-place and task waiting.
 
-We could have allowed "others" array aggregates, by adding after
-4.3.3(15.1):
-
-        For a declare_expression, the applicable index constraint for
-        the *body*_expression is that, if any, defined for the
-        declare_expression.
-
 If we allowed limited types, we would probably need to update 7.5(2.1).
 
 A declare expression cannot be static or predicate-static
@@ -155,19 +179,20 @@
 !examples
 
    Post => Fun'Result =
-      (declare X : constant T1 := F(A, B); Y : constant T2 := G(C, D); begin
-         (if X > Y then X else Y+X))
+      (declare X : constant T1 := F(A, B); Y : constant T2 := G(C, D);
+       begin   (if X > Y then X else Y+X))
 
    Type_Invariant =>
-      (M : constant Integer := Integer'Max(T.A, T.B); begin
-        (if M > 0 then M > T.C else M < T.D))
+      (declare M : constant Integer := Integer'Max(T.A, T.B);
+       begin   (if M > 0 then M > T.C else M < T.D))
 
    Dynamic_Predicate =>
       (declare Q : constant Integer := H(S.A, S.B);
-               R : constant Integer := G(S.C, S.D); begin
-          (if W(Q, R) then F(Q) else Z(R)));
+               R : constant Integer := G(S.C, S.D);
+       begin
+          (if W(Q, R) then F(Q) else Z(R)))
 
-    X : T := (declare Temp renames Some_Array(Y..Z)
+    X : T := (declare Temp renames Some_Array(Y..Z);
               begin Temp & Temp);
 
 The example in the !problem:
@@ -189,7 +214,7 @@
 
 !ASIS
 
-** TBD.
+New ASIS queries are needed. Those are TBD.
 
 !ACATS test