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
Questions? Ask the ACAA Technical Agent