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

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

--- ai12s/ai12-0239-1.txt	2019/07/05 22:59:43	1.3
+++ ai12s/ai12-0239-1.txt	2019/10/01 23:47:33	1.4
@@ -1,4 +1,4 @@
-!standard 11.4.1(27/3)                                  19-06-15  AI12-0239-1/02
+!standard 11.4.1(27/3)                                19-10-01   AI12-0239-1/03
 !class Amendment 17-10-05
 !status work item 17-10-05
 !status received 17-10-03
@@ -24,7 +24,7 @@
 instrumentation code in the final executable.
 
 Additionally, fine-grained control over ghost code may be useful for
-traceability  and debugging.
+traceability and debugging.
 
 !proposal
 
@@ -38,10 +38,15 @@
    "ghost variable" are defined analogously (e.g., a function whose Ghost
    aspect is True is said to be a ghost function). In addition, a subcomponent
    of a ghost object is a ghost object.
+
+   Ghost policies are a class of assertion aspect and can only be specified
+   within the Ghost_Assertion_Policy pragma as part of a list of Ghost_Ids with
+   their associated Assertion_Policy. Ghost_Ids within an Ghost_Assertion_Policy
+   pragma shall either be user-defined ghost policies or the default policy of
+   Ghost. [This means that Ghost can be named in a Ghost_Assertion_Policy pragma.]
 
-   Ghost is an assertion aspect, and unique identifiers within an
-   Assertion_Policy pragma shall be user-defined ghost policies.
-   [This means that Ghost can be named in an Assertion_Policy pragma.]
+   When Ghost_Policy is not specified for a ghost entity its policy shall be
+   Ghost.
 
    Ghost_Policy may appear on an entity without Ghost defined in which case
    it is assumed that Ghost shall be in effect for said entity (e.g. equivalent
@@ -90,10 +95,13 @@
    aspect_specification for an object_declaration having more than one
    defining_identifier), a package, or a generic package.
 
-   The Ghost aspect may be specified via either an aspect_specification
-   or via a pragma. The representation pragma Ghost takes a single
-   argument, a name denoting one or more entities whose Ghost aspect is
-   then specified to be True.
+   The Ghost and Ghost_Policy aspect may be specified via either an
+   aspect_specification or via a pragma. The representation pragma Ghost
+   takes a single argument, a name denoting one or more entities whose Ghost
+   aspect is then specified to be True. The representation pragma Ghost_Policy
+   takes two arguments, a name denoting one or more Ghost entities or entities
+   whose Ghost aspect is specified as true, and a ghost assertion policy
+   identifier.
 
    [In particular, Ada does not currently include any form of
    ghost components of non-ghost record types, or ghost parameters of
@@ -103,18 +111,13 @@
    except in a confirming aspect specification. [For example, a
    non-ghost declaration cannot occur within a ghost subprogram.]
 
-   The value specified for a Ghost assertion policy in an
-   Assertion_Policy pragma shall be either Check or Ignore.
+   The value specified for a Ghost assertion policy in a
+   Ghost_Assertion_Policy pragma shall be either Check or Ignore.
    [In other words, implementation-defined assertion policy values
-   are not permitted.] The Ghost assertion policy in effect at any
+   are not permitted.] The Ghost assertion policies in effect at any
    point of an Ada program shall be either Check or Ignore.
-
-7.  A ghost type or object shall not be effectively volatile.
-    A ghost object shall not be imported or exported.
-    [In other words, no ghost objects for which reading or writing
-    would constitute an external effect (see Ada RM 1.1.3).]
 
-8.  A ghost primitive subprogram of a non-ghost type extension shall
+7.  A ghost primitive subprogram of a non-ghost type extension shall
     not override an inherited non-ghost primitive subprogram.
     A non-ghost primitive subprogram of a type extension shall
     not override an inherited ghost primitive subprogram.
@@ -123,7 +126,7 @@
     progenitor; primitive subprograms of such a type may override
     inherited (ghost or non-ghost) subprograms.]
 
-9.  A Ghost pragma which applies to a declaration occurring
+8.  A Ghost pragma which applies to a declaration occurring
     in the visible part of a package shall not occur in the
     private part of that package.
 
@@ -131,24 +134,24 @@
     can be determined without having to look into the private part of
     the enclosing package.]
 
-10. A ghost entity shall only be referenced:
+9. A ghost entity shall only be referenced:
 
-    * from within an assertion expression; or
+   * from within an assertion expression; or
 
-    * from within an aspect specification [(i.e., either an
-      aspect_specification or an aspect-specifying pragma)]; or
+   * from within an aspect specification [(i.e., either an
+     aspect_specification or an aspect-specifying pragma)]; or
 
-    * within the declaration or completion of a ghost entity
-      (e.g., from within the body of a ghost subprogram); or
+   * within the declaration or completion of a ghost entity
+     (e.g., from within the body of a ghost subprogram); or
 
-    * within a ghost statement; or
+   * within a ghost statement; or
 
-    * within a with_clause or use_clause; or
+   * within a with_clause or use_clause; or
 
-    * within a renaming_declaration which either renames a ghost entity
-      or occurs within a ghost subprogram or package.
+   * within a renaming_declaration which either renames a ghost entity
+     or occurs within a ghost subprogram or package.
 
-11. A ghost entity shall not be referenced within an aspect
+10. A ghost entity shall not be referenced within an aspect
     specification [(including an aspect-specifying pragma)]
     which specifies an aspect of a non-ghost entity except in the
     following cases:
@@ -162,14 +165,14 @@
       refer to a ghost variable.]
 
    [Predicate expressions are excluded because predicates participate
-   in membership tests; no Assertion_Policy pragma has any effect on
+   in membership tests; no Ghost_Assertion_Policy pragma has any effect on
    this participation. In the case of a Static_Predicate expression,
    there are also other reasons (e.g., case statements).]
 
-12. An out or in out mode actual parameter in a call to a ghost
+11. An out or in out mode actual parameter in a call to a ghost
     subprogram shall be a ghost variable.
 
-13. If the Ghost assertion policy in effect at the point of the
+12. If the Ghost assertion policy in effect at the point of the
     declaration of a ghost entity is Ignore, then the Ghost assertion
     policy in effect at the point of any reference to that entity shall
     be Ignore.
@@ -182,7 +185,7 @@
     [This includes both assignment statements and passing a ghost
     variable as an out or in out mode actual parameter.]
 
-14. An Assertion_Policy pragma specifying a Ghost assertion policy
+13. A Ghost_Assertion_Policy pragma specifying Ghost assertion policies
     shall not occur within a ghost subprogram or package.
     If a ghost entity has a completion then the Ghost assertion policies
     in effect at the declaration and at the completion of the entity
@@ -193,27 +196,23 @@
     declaration of an entity and at the point of an aspect specification
     which applies to that entity shall be the same.
 
-15. The Ghost assertion policies in effect at the declaration of a
-    state abstraction and at the declaration of each constituent of that
-    abstraction shall be the same.
-
-16. The Ghost assertion policies in effect at the declaration of a
+14. The Ghost assertion policies in effect at the declaration of a
     primitive subprogram of a ghost tagged type and at
     the declaration of the ghost tagged type shall be the same.
 
-17. If a tagged type is not a disabled ghost type, and if a
+15. If a tagged type is not a disabled ghost type, and if a
     primitive operation of the tagged type overrides an inherited
     operation, then the corresponding operation of the ancestor type
     shall be a disabled ghost subprogram if and only if the overriding
     subprogram is a disabled ghost subprogram.
 
-18. If the Ghost assertion policy in effect at the point of
+16. If the Ghost assertion policy in effect at the point of
     a reference to a Ghost entity which occurs within an assertion
     expression is Ignore, then the assertion policy which governs the
     assertion expression (e.g., Pre for a precondition expression,
     Assert for the argument of an Assert pragma) shall [also] be Ignore.
 
-19. A ghost type shall not have a task or protected part.
+17. A ghost type shall not have a task or protected part.
     A ghost object shall not be of a type which yields synchronized
     objects.
     A ghost object shall not have a volatile part.
@@ -336,9 +335,9 @@
 From: Steve Baird
 Sent: Tuesday, October 3, 2017  9:49 AM
 
-> If the Ghost assertion policy in effect at the point of the 
-> declaration of a ghost entity is Ignore, then the Ghost assertion 
-> policy in effect at the point of any reference to that entity shall be 
+> If the Ghost assertion policy in effect at the point of the
+> declaration of a ghost entity is Ignore, then the Ghost assertion
+> policy in effect at the point of any reference to that entity shall be
 > Ignore.
 
 I forgot to mention the issue of enforcing rules such as the one cited above
@@ -448,10 +447,10 @@
 
 [Version /02 of the AI was attached to this message - Editor.]
 
-As one of my first serious AI assignments it shall be likely that I am 
+As one of my first serious AI assignments it shall be likely that I am
 missing something or that other revisions be necessary : )
 
-I will need to modify the semantics of Assertion_Policy, but I first wanted 
+I will need to modify the semantics of Assertion_Policy, but I first wanted
 to check the consensus of the group first.
 
 The most relevant section is below:
@@ -462,18 +461,18 @@
 
 !problem
 
-Sometimes, the variables and functions that are present in a program are not 
-sufficient to specify intended properties. In such a case, it would be 
-desirable to have the possibility to insert in the program additional code 
-useful for specification and verification, specially identified so that it 
-can be discarded during compilation. So-called ghost code are these parts of 
-the code that are only meant for specification and verification, and have no 
-effect on the functional behavior of the program. The goal is to have more 
-assurance that a given instrumentation of a program for verification purposes 
-does not interfere with the program being instrumented, and of the removal of 
+Sometimes, the variables and functions that are present in a program are not
+sufficient to specify intended properties. In such a case, it would be
+desirable to have the possibility to insert in the program additional code
+useful for specification and verification, specially identified so that it
+can be discarded during compilation. So-called ghost code are these parts of
+the code that are only meant for specification and verification, and have no
+effect on the functional behavior of the program. The goal is to have more
+assurance that a given instrumentation of a program for verification purposes
+does not interfere with the program being instrumented, and of the removal of
 instrumentation code in the final executable.
 
-Additionally, fine-grained control over ghost code may be useful for 
+Additionally, fine-grained control over ghost code may be useful for
 traceability and debugging.
 
 !proposal
@@ -494,7 +493,7 @@
     [This means that Ghost can be named in an Assertion_Policy pragma.]
 
     Ghost_Policy may appear on an entity without Ghost defined in which case
-    it is assumed that Ghost shall be in effect for said entity (e.g. 
+    it is assumed that Ghost shall be in effect for said entity (e.g.
     equivalent to with Ghost => True).
 
 ****************************************************************
@@ -506,16 +505,16 @@
 >     Assertion_Policy pragma shall be user-defined ghost policies.
 >     [This means that Ghost can be named in an Assertion_Policy pragma.]
 
-I don't quite understand why " unique identifiers within an Assertion_Policy 
-pragma shall be user-defined ghost policies." I didn't see any other mention 
-of the idea of "user-defined ghost policies". 
+I don't quite understand why " unique identifiers within an Assertion_Policy
+pragma shall be user-defined ghost policies." I didn't see any other mention
+of the idea of "user-defined ghost policies".
 
 >     Ghost_Policy may appear on an entity without Ghost defined in which case
->     it is assumed that Ghost shall be in effect for said entity (e.g. 
+>     it is assumed that Ghost shall be in effect for said entity (e.g.
 >     equivalent to with Ghost => True).
 
-What is the purpose of Ghost_Policy, if we already have Ghost as a new 
-Assertion_Policy identifier? I also didn't see Ghost_Policy mentioned anywhere 
+What is the purpose of Ghost_Policy, if we already have Ghost as a new
+Assertion_Policy identifier? I also didn't see Ghost_Policy mentioned anywhere
 else. So it looks like all it does is affect the Ghost aspect to also be true,
 so it seems totally redundant.
 
@@ -527,27 +526,27 @@
 >>      Ghost is an assertion aspect, and unique identifiers within an
 >>      Assertion_Policy pragma shall be user-defined ghost policies.
 >>      [This means that Ghost can be named in an Assertion_Policy pragma.]
-> I don't quite understand why " unique identifiers within an Assertion_Policy 
-> pragma shall be user-defined ghost policies." I didn't see any other mention 
+> I don't quite understand why " unique identifiers within an Assertion_Policy
+> pragma shall be user-defined ghost policies." I didn't see any other mention
 > of the idea of "user-defined ghost policies".
 
-Yes, I agree, I need to go into more detail about what ghost policies are and 
-how they interact with the ghost aspect. In short the intention was to allow 
+Yes, I agree, I need to go into more detail about what ghost policies are and
+how they interact with the ghost aspect. In short the intention was to allow
 categories of ghost so that they can be selectively turned on or off. Entities
-marked simply with "Ghost" will be in the general policy of Ghost while 
-additional user-defined policies will act independently and will be indicated 
+marked simply with "Ghost" will be in the general policy of Ghost while
+additional user-defined policies will act independently and will be indicated
 with the new aspect Ghost_Policy.
 
 >>      Ghost_Policy may appear on an entity without Ghost defined in which case
 >>      it is assumed that Ghost shall be in effect for said entity (e.g.
 >>      equivalent to with Ghost => True).
-> What is the purpose of Ghost_Policy, if we already have Ghost as a new 
-Assertion_Policy identifier? I also didn't see Ghost_Policy mentioned anywhere 
-else. So it looks like all it does is affect the Ghost aspect to also be true, 
+> What is the purpose of Ghost_Policy, if we already have Ghost as a new
+Assertion_Policy identifier? I also didn't see Ghost_Policy mentioned anywhere
+else. So it looks like all it does is affect the Ghost aspect to also be true,
 so it seems totally redundant.
 
-It would not be redundant since Ghost takes a boolean and thus could have some 
-sort of static expression which could lead to it being False. 
+It would not be redundant since Ghost takes a boolean and thus could have some
+sort of static expression which could lead to it being False.
 Ghost_Policy takes an identifier and would lose this capability.
 
 ****************************************************************
@@ -556,5 +555,74 @@
 Sent: Sunday, June 16, 2019  10:03 AM
 
 Thanks Justin for a good start on this AI!  Has promise ...
+
+****************************************************************
+
+From: Justin Squirek
+Sent: Tuesday, October 1, 2019  2:43 PM
+
+Here is my homework for the upcoming meeting
+
+[This was a copy of version /02 - Editor.]
+
+****************************************************************
+
+From: Justin Squirek
+Sent: Tuesday, October 1, 2019  3:27 PM
+
+I previously sent the wrong version. Please disregard that one and use this
+one in its place.
+
+[This is version /03 of the AI - Editor.]
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, October 1, 2019  4:00 PM
+
+Looks very good.  However, in an AI, we don't usually number the paragraphs of
+a new section.  Was that intentional or a side effect of some formatting tool?
+And the numbers are only on top-level paragraphs, which is definitely not our
+usual formatting approach.
+
+****************************************************************
+
+From: Justin Squirek
+Sent: Tuesday, October 1, 2019  4:17 PM
+
+No, I was keeping in the style of the original AI. Which I guess was rougher
+than I assumed. Please disregard extraneous formatting.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 1, 2019  4:32 PM
+
+I think Tucker is confusing !wording with !proposal. I agree that we usually
+don't number paragraphs, but it was done here as there are so many separate
+topics. And !proposal is free-form, so there's no reason to avoid numbering
+if it makes it easier to refer to a particular topic. Presumably that would
+be removed once it was replaced with actual wording.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 1, 2019  6:46 PM
+
+A couple of thoughts about this proposal:
+
+(1) We haven't defined any new pragmas that apply to entities, as we think that
+using aspects for such usages is  preferred. So I don't think we need or want
+pragmas Ghost and Ghost_Policy. (GNAT can define such things if it wants.) We do
+need the Ghost_Assertion_Policy pragma, as that is a more global thing.
+
+(2) I didn't see anything where the text describes the use of user-defined ghost
+"policies". They just sort of appear. I suspect that we need a different name
+for these (they're not policies, they're sets of entities to which a policy
+applies -- the policy is "Check" or "Ignore"). In particular, I find the
+difference between "Ghost_Policy" and "Ghost_Assertion_Policy" confusing, for
+this reason (the latter sets a policy, the former names the set to which a
+policy applies - perhaps "Ghost_Set" is the appropriate name for the former, and
+then we can use Ghost_Policy for the latter??)
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent