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

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

--- ai12s/ai12-0187-1.txt	2016/10/03 03:57:29	1.4
+++ ai12s/ai12-0187-1.txt	2016/12/28 04:20:39	1.5
@@ -67,14 +67,14 @@
 view, and on primitive subprograms. (It's not allowed on formal types, since
 it is only meaningful for primitive subprograms.) The intent is that the
 subprogram version be used to override the type version when necessary; it
-is very useful as a stand-alone aspect (it makes more sense to just modify
+is not very useful as a stand-alone aspect (it makes more sense to just modify
 the postcondition in that case).
 
 For a type, the value of the aspect is a list of function names. The named
 functions must be property functions. For a primitive subprogram, the value
 of the aspect is either a list of function names, or a list of items, each being
-"not" followed by a function name; again all of the functions need to be property
-names.
+"not" followed by a function name; again all of the functions need to be names of
+property functions.
 
     AARM Ramification: For a subprogram, the functions all have "not" or none
     do; mixing "not" functions with regular functions is not allowed.
@@ -93,7 +93,8 @@
 the Stable_Property aspect of S shall be a stable property function of a type
 for which S is primitive.
 
-The *stable property functions for type T" for a primitive subprogram S of T are:
+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",
@@ -104,8 +105,7 @@
 
    AARM Discussion: A primitive subprogram can be primitive for more than one
    type, and thus there can be more than one such set of stable properties
-   for a subprogram. This is likely to be very rare, so we try to ignore the
-   possibility in the rules.
+   for a subprogram. Thus we say "stable property functions for S for type T".
 
 For every primitive subprogram S of a type T that is not a stable property
 function of T, the actual postcondition of S includes expressions of the form
@@ -182,7 +182,7 @@
 
 (4) I went with the simple rule for postconditions: any mention of any
 stable property function in the postcondition turns off the automatic
-stable property condition for that functions. I could have used a more detailed
+stable property condition for that function. I could have used a more detailed
 rule requiring the stable property function to have a parameter of the type
 from the subprogram in question, and even treated the properties differently
 if there are multiple such parameters. While that would get better results in

Questions? Ask the ACAA Technical Agent