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