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

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0236-1.txt

--- ai12s/ai12-0236-1.txt	2017/09/07 02:38:59	1.1
+++ ai12s/ai12-0236-1.txt	2018/01/27 03:04:57	1.2
@@ -1,4 +1,4 @@
-!standard 13.11(5)                                  17-09-06  AI12-0236-1/01
+!standard 13.11(5)                                  18-01-26  AI12-0236-1/02
 !standard 13.11.4(3/3)
 !class Amendment 17-09-06
 !status work item 17-09-06
@@ -20,8 +20,8 @@
 to bind the result of an expression - for example a function call - to a name,
 in order to reuse its value.
 
-This often leads to repeating the same expression/function call several time
-within contracts.
+This often leads to repeating the same expression several times within
+contracts.
 
 Take the following subprogram and its post-condition into consideration:
 
@@ -43,93 +43,77 @@
 
 !proposal
 
-[Editor's note: I've defined the syntax to follow that of a block, thus minimizing
-differences from other kinds of declarations. This is sort of like Raphael's proposal,
-but with all of the unnecessary differences removed. The following is pseudo-wording:]
+A *declare expression* allows constant objects and renamings of constants to be
+declared within an expression.
 
-A *declare expression* allows defining names for parts of expressions.
+!wording
 
 Syntax
+
+declare_expression ::= (declare {declare_item} begin *body*_expression)
+
+declare_item ::= constant_declare_item | renaming_declare_item
+
+constant_declare_item ::=
+    defining_identifier_list : constant [subtype_indication] := expression;
+
+renaming_declare_item ::=
+    defining_identifier [: [null_exclusion] subtype_mark] renames object_name;
+
+[TBD: Should aspect_specifications be allowed on declare_items?
 
-declare_expression ::= ([declare] declare_item {; declare_item} begin *body*_expression)
+Should we allow access_definition in declare_items?  I think not.
 
-declare_item ::= defining_identifier : constant [subtype_indication] := expression
+Should we allow "aliased" in constant_declare_items?
 
+Should we allow array_type_definition in constant_declare_items?  I think not.
+
+I'm allowing multiple identifiers in constant_declare_items, for uniformity with
+object_declarations.
+
+I'm allowing "(declare begin expression)" with no declare_items, for uniformity
+with block statements, which also annoyingly allow a pointless "declare".]
+
 Static Semantics
+
+The scope of a defining_identifier of a declare_item is the enclosing
+declare_expression. The semantics of a declare_item are the same as an
+object_declaration or object_renaming_declaration of the same form.
+
+[TBD: The above is intended to include static semantics, name resolution,
+legality, and dynamic semantics.
 
-A *typed declarative expression* is either:
-   * a name statically denoting a stand-alone object;
-   * a qualified expression;
-   * a type conversion;
-   * a parenthesized expression whose operand is a typed declarative expression;
-   * a conditional expression where at least one operand is a typed declarative
-     expression;
-   * a predefined operator other than & where at least one operand is a
-     typed declarative expression;
-   * a slice or indexed_component of a typed declarative expression;
-   * a selected_component that denotes a component of a typed declarative expression.
-
-AARM Reason: In all of these cases, the type of the expression is uniquely
-determined by the contents of the expression.
-
-The view defined by the defining_identifier of a declare_item is constant.
-
-The scope of the defining_identifier of a declare_item is the enclosing
-declare_expression.
-
-Legality Rules
-
-The subtype_indication of a declare_item shall be present if the expression of the
-declare_item is not a typed declarative expressions.
-
-AARM Reason: We allow omitting the type name only if it is certain to be
-unnecessary to resolve the expression. In other cases, especially those
-involving universal types, the expression could resolve to a type other than
-that intended.
-
-[Editor's note: Here's an example.
-
-    MAX : constant := 1000;
-
-    procedure Foobar (Some_Param : Natural; ...) with
-       Pre => (X : constant := (if Some_Param > MAX then MAX else 10) begin
-           (if Some_Param > X then ...)) is
-
-Here, X will resolve to have type root_integer, as it is not a static
-expression and thus the preference to root_integer will apply. But that
-makes the comparison to Some_Param illegal, since root_integer is not the
-same type as Natural. If the subtype name Natural is given in the declaration
-of X, all is well.
+I am assuming another AI will define the semantics of:
 
-End Editor's note.]
+    X: constant := expression; -- not as a named number!
+    Y renames expression;
 
+i.e. an object_declaration without a subtype_indication (must include
+"constant"), and an object_renaming_declaration without a subtype_mark
+(expression must denote a constant view).
+
+That AI should contain the business about *typed declarative expression*, which
+allows to distinguish number_declarations from object_declarations.
+]
+
 Name Resolution Rules
 
 The type of a declare_expression is the type of the *body*_expression.
 
-4.5.7(8/3) is used here with "conditional_expression" replaced by
-"declare_expression" and "*dependent_*expression" replaced by
-"*body_*expression". (This discusses expected types, but not everything
-has an expected type.
-
-The expected type for the expression of a declare_item is that of the
-subtype_indication if present and any type otherwise.
-
-Dynamic Semantics
+If a declare_expression is expected to be of a type T, then the
+*body*_expression is expected to be of type T. Similarly, if a
+declare_expression is expected to be of some class of types, then the
+*body*_expression is subject to the same expectation. If a declare_expression
+shall resolve to be of a type T, then the *body*_expression shall resolve to be
+of type T.
 
-For the evaluation of a declare_expression, the declare_items are
-elaborated and then the *body_*expression is evaluated.
+[TBD: Above rule comes from 4.5.7(8/3) for conditional_expressions.]
 
-For the elaboration of a declare_item, the subtype_indication (if
-any) is elaborated first, then the expression is evaluated and
-converted to the type of the object, and then the expression is
-assigned to the object. [Editor's note: This is a simplified
-version of the rules for an object declaration; perhaps there
-is some way to use those directly??]
-
-!wording
+Dynamic Semantics
 
-** TBD.
+For the evaluation of a declare_expression, the declare_items are elaborated and
+then the *body_*expression is evaluated. The value of the declare_expression is
+that of the *body_*expression.
 
 !discussion
 
@@ -137,30 +121,39 @@
 
 !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))
+   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))
 
    Type_Invariant =>
-      (M : constant := IntegeríMax(T.A, T.B) begin
+      (M : constant := Integer'Max(T.A, T.B); begin
         (if M > 0 then M > T.C else M < T.D))
 
+[TBD: I inherited the above example, but it seems to be illegal, because the
+call to 'Max is not a "typed declarative expression".  Perhaps it should be
+legal, but it seems like that's the subject of another AI.]
+
    Dynamic_Predicate =>
       (declare Q : constant Integer := H(S.A, S.B);
-               R : constant Integer := G(S.C, S.D) begin
+               R : constant Integer := G(S.C, S.D); begin
           (if W(Q, R) then F(Q) else Z(R)));
 
-The example in the !problem:
+    X : T := (declare Temp renames Some_Array(Y..Z)
+              begin Temp & Temp);
 
+The example in the !problem (assuming Cur_Position is a name statically denoting
+a stand-alone object, and therefore a typed declarative expression):
+
    procedure Fgetc (Stream : File_Descr; Result : out Int) with
      Post =>
-       (declare The_Char : constant Character := The_File (Cur_Position'Old)
-                Pos_Unchg : constant Boolean := Cur_Position = Cur_Position'Old
+       (declare
+          The_Char : constant Character := The_File (Cur_Position'Old);
+          Pos_Unchg : constant := Cur_Position = Cur_Position'Old;
         begin
            (if The_Char = EOF_Ch
-            then Pos_Unchg and then Result = EOF
+              then Pos_Unchg and then Result = EOF
             elsif The_Char = ASCII.LF
-            then Pos_Unchg and then Result = Character'Pos (ASCII.LF)
+              then Pos_Unchg and then Result = Character'Pos (ASCII.LF)
             else
               Cur_Position = Cur_Position'Old + 1
               and then Result = Character'Pos (The_File (Cur_Position'Old))));
@@ -173,7 +166,6 @@
 
 ACATS B-Test and C-Tests are needed to check that the new capabilities are
 supported.
-
 
 !appendix
 

Questions? Ask the ACAA Technical Agent