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

Differences between 1.9 and version 1.10
Log of other versions for file ai12s/ai12-0187-1.txt

--- ai12s/ai12-0187-1.txt	2017/11/30 04:18:02	1.9
+++ ai12s/ai12-0187-1.txt	2017/12/09 04:48:12	1.10
@@ -1,4 +1,4 @@
-!standard 7.3.3(0)                                    17-11-21  AI12-0187-1/06
+!standard 7.3.3(0)                                    17-12-07  AI12-0187-1/07
 !standard 13.1.1(4/3)
 !class Amendment 16-06-02
 !status Amendment 1-2012 17-11-21
@@ -25,8 +25,7 @@
 "invariant" already has a meaning. "Immutable" and "constant" also have been
 used, plus all of those need the prefix "usually" to weaken them. "Stable"
 doesn't seem to suffer from either of these problems; my car's oil may be
-stable, but I still change it periodically. Anyway, the exact name isn't
-critical.]
+stable, but I still change it periodically.]
 
 For instance, for I/O, the open status of a file and the mode of a file are 
 stable properties (only being changed by a few routines: Open, Create, Close,
@@ -105,10 +104,10 @@
 Static Semantics
 
   A *property function* of type T is a function with a single parameter of
-  type T or class-wide type that covers T.
+  type T or of a class-wide type that covers T.
 
   AARM Reason: This provides restrictions on name resolution so overloaded functions
-  can be used.
+  can be used as a stable property function.
 
   For a private type, private extension, or full type that does not have a
   partial view, the following language-defined aspects may be specified with an
@@ -177,7 +176,7 @@
 
   A stable property function of a type T (including a class-wide stable property
   function) shall have a nonlimited return type and shall be:
-     * a primitive function with a single parameter of mode *in* of type T; or
+     * a primitive function with a single parameter of mode /in/ of type T; or
      * a function that is declared immediately within the declarative region in
        which an ancestor type of T is declared and has a single parameter of mode
        *in* of a class-wide type that covers T.
@@ -185,8 +184,8 @@
   In a subprogram_property_aspect_definition for a subprogram S:
     * all or none of the items shall be preceded by /not/;
 
-    AARM Ramification: The listed functions all have /not/ or none
-      do; mixing /not/ functions with regular functions is not allowed.
+    AARM Ramification: Mixing /not/ functions with regular functions is not
+      allowed.
 
     * any property functions mentioned after /not/ shall be a stable property
       function of a type for which S is primitive.
@@ -195,12 +194,13 @@
 
 For a primitive subprogram S of a type T, the stable property functions for S for
 type T are:
-   * if S has an aspect Stable_Properties specified that does not include "not",
-     those functions denoted in the aspect Stable_Properties for S;
-   * if S has an aspect Stable_Properties specified that includes "not",
+   * if S has an aspect Stable_Properties specified that does not include /not/,
+     those functions denoted in the aspect Stable_Properties for S that have a
+     parameter of T or T'Class;
+   * if S has an aspect Stable_Properties specified that includes /not/,
      those functions denoted in the aspect Stable_Properties for T, excluding
      those denoted in the aspect Stable_Properties for S;
-   * if does not have an aspect Stable_Properties, those functions denoted in
+   * if S does not have an aspect Stable_Properties, those functions denoted in
      the aspect Stable_Properties for T, if any.
 
    AARM Discussion: A primitive subprogram can be primitive for more than one
@@ -213,7 +213,7 @@
 
 The *explicit* specific postcondition expression for a subprogram S is the
 expression directly specified for S with the Post aspect. Similarly, the
-*explicit* specific postcondition expression for a subprogram S is the
+*explicit* class-wide postcondition expression for a subprogram S is the
 expression directly specified for S with the Post'Class aspect. 
 
 For every primitive subprogram S of a type T that is not a stable property
@@ -227,10 +227,10 @@
 when interpreting the meaning of the postcondition as defined in 6.1.1].
 
    AARM Ramification: There is one F(P) = F(P)'Old subexpression for every
-   combination of stable expression function of type T and parameter of type T.
-   For instance, if there is three stable property functions for type T and two
-   parameters of type T, then there are six such subexpressions appended to the
-   postcondition.
+   combination of a stable expression function of type T and a parameter of
+   type T. For instance, if there is three stable property functions for type T
+   and two parameters of type T, then there are six such subexpressions
+   appended to the postcondition.
 
    The resulting specific postcondition is evaluated as described in 6.1.1.
    One hopes that compilers can be smart enough to prove that many of these
@@ -260,7 +260,7 @@
    postcondition IS the class-wide postcondition for S, and therefore
    inherited postconditions include any stable property expressions.
 
-Modify 13.1.1(4/3):
+Replace 13.1.1(4/3) by:
 
    aspect_definition ::= name | expression | identifier |
                          type_property_aspect_definition |
@@ -412,6 +412,136 @@
        ...
 
     end Ada.Text_IO;
+
+!corrigendum 7.3.3(0)
+
+@dinsc
+
+It is usual that some of the characteristics of a data type are unchanged by
+most of the primitive operations on the type. Such characteristics are called
+@i<stable properties> of the type.
+
+@s8<@i<Syntax>>
+
+@xcode<@fa<type_property_aspect_definition>@fa< ::= >@fa<name>@fa< {, >@fa<name>@fa<}>>
+
+@xcode<@fa<subprogram_property_aspect_definition>@fa< ::= [>@ft<@b<not>>@fa<] >@fa<name>@fa< {, [>@ft<@b<not>>@fa<] >@fa<name>@fa<}>>
+
+@s8<@i<Static Semantics>>
+
+A @i<property function> of type @i<T> is a function with a single parameter of
+type @i<T> or of a class-wide type that covers @i<T>.
+
+For a private type, private extension, or full type that does not have a
+partial view, the following language-defined aspects may be specified with an
+@fa<aspect_specification> (see 13.1.1):
+
+@xhang<@xterm<Stable_Properties>This aspect
+  shall be specified by a @fa<type_property_aspect_definition>; each
+  @fa<name> shall statically denote a single property function of the type. This
+  aspect defines the @i<stable property functions> of the associated type.>
+
+@xhang<@xterm<Stable_Properties'Class>This aspect
+    shall be specified by a @fa<type_property_aspect_definition>; each
+    @fa<name> shall statically denote a single property function of the type. This
+    aspect defines the @i<class-wide stable property functions> of the associated type.
+    Unlike most class-wide aspects, Stable_Properties'Class is not
+    inherited by descendant types and subprograms, but the enhanced class-wide
+    postconditions are inherited in the normal manner.>
+
+For a primitive subprogram, the following language-defined aspects may be
+specified with an @fa<aspect_specification> (see 13.1.1):
+
+@xhang<@xterm<Stable_Properties>This aspect
+    shall be specified by a @fa<subprogram_property_aspect_definition>;
+    each @fa<name> shall statically denote a single property function of a type for
+    which the associated subprogram is primitive.>
+
+@xhang<@xterm<Stable_Properties'Class>This aspect
+    shall be specified by a @fa<subprogram_property_aspect_definition>;
+    each @fa<name> shall statically denote a single property function of a tagged
+    type for which the associated subprogram is primitive. Unlike most
+    class-wide aspects, Stable_Properties'Class is not inherited by descendant
+    subprograms, but the enhanced class-wide postconditions are inherited in
+    the normal manner.>
+
+@s8<@i<Legality Rules>>
+
+A stable property function of a type @i<T> (including a class-wide stable property
+function) shall have a nonlimited return type and shall be:
+
+@xbullet<a primitive function with a single parameter of mode @b<in> of
+type @i<T>; or>
+
+@xbullet<a function that is declared immediately within the declarative region
+in which an ancestor type of @i<T> is declared and has a single parameter of
+mode @b<in> of a class-wide type that covers @i<T>.>
+
+In a @fa<subprogram_property_aspect_definition> for a subprogram @i<S>:
+
+@xbullet<all or none of the items shall be preceded by @b<not>;>
+
+@xbullet<any property functions mentioned after @b<not> shall be a stable
+property function of a type for which @i<S> is primitive.>
+
+@s8<@i<Static Semantics>>
+
+For a primitive subprogram @i<S> of a type @i<T>, the stable property functions
+for @i<S> for type @i<T> are:
+
+@xbullet<if @i<S> has an aspect Stable_Properties specified that does not
+include @b<not>, those functions denoted in the aspect Stable_Properties for
+@i<S> that have a parameter of @i<T> or @i<T>'Class;>
+
+@xbullet<if @i<S> has an aspect Stable_Properties specified that includes
+@b<not>, those functions denoted in the aspect Stable_Properties for @i<T>,
+excluding those denoted in the aspect Stable_Properties for @i<S>;>
+
+@xbullet<if @i<S> does not have an aspect Stable_Properties, those functions
+denoted in the aspect Stable_Properties for @i<T>, if any.>
+
+A similar definition applies for class-wide stable property functions by
+replacing aspect Stable_Properties with aspect Stable_Properties'Class
+in the above definition.
+
+The @i<explicit> specific postcondition expression for a subprogram @i<S>
+is the @fa<expression> directly specified for @i<S> with the Post aspect.
+Similarly, the @i<explicit> class-wide postcondition expression for a
+subprogram @i<S> is the @fa<expression> directly specified for @i<S> with the
+Post'Class aspect. 
+
+For every primitive subprogram @i<S> of a type @i<T>
+that is not a stable property function of @i<T>, the specific postcondition
+expression of @i<S> is modified to include expressions of the form
+@fc<@i<F>(@i<P>) = @i<F>(@i<P>)'Old>, all @b<and>ed with each other
+and any explicit specific postcondition expression, where @i<F> is each stable
+property function of @i<S> for type @i<T> that does not occur in the explicit
+specific postcondition expression of @i<S>, and @i<P> is each parameter of
+@i<S> that has type @i<T>. The resulting specific postcondition expression of
+@i<S> is used in place of the explicit specific postcondition expression of
+@i<S> when interpreting the meaning of the postcondition as defined in 6.1.1.
+
+For every primitive subprogram @i<S> of a type @i<T>
+that is not a stable property function of @i<T>, the class-wide postcondition
+expression of @i<S> is modified to include expressions of the form
+@fc<@i<F>(@i<P>) = @i<F>(@i<P>)'Old>, all @b<and>ed with each other and any
+explicit class-wide postcondition expression, where @i<F> is each class-wide
+stable property function of @i<S> for type @i<T> that does not occur in any
+class-wide postcondition expression that applies to @i<S>, and @i<P> is each
+parameter of @i<S> that has type @i<T>. The resulting class-wide postcondition
+expression of @i<S> is used in place of the explicit class-wide postcondition
+expression of @i<S> when interpreting the meaning of the
+postcondition as defined in 6.1.1.
+
+!corrigendum 13.1.1(4/3)
+
+@drepl
+@xcode<@fa<aspect_definition ::= name | expression | identifier>>
+@dby
+@xcode<@fa<aspect_definition>@fa< ::=>
+   @fa<name>@fa< | >@fa<expression>@fa< | >@fa<identifier>@fa< |>
+   @fa<type_property_aspect_definition>@fa< |>
+   @fa<subprogram_property_aspect_definition>>
 
 !ASIS
 

Questions? Ask the ACAA Technical Agent