CVS difference for 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