Version 1.4 of ai05s/ai05-0250-1.txt
!standard 7.3.2(0) 11-09-27 AI05-0250-1/03
!standard 3.9.2(20.2/2)
!class Amendment 11-06-15
!status Amendment 2012 11-07-27
!status ARG Approved 10-0-1 11-06-26
!status work item 11-06-15
!status received 11-06-15
!priority Low
!difficulty Easy
!subject Thoughts on type invariants
!summary
Specific Invariants can be hidden (given on the full declaration of a private type).
The places at which invariant checks are performed are clarified.
!question
1) It would be useful to have the option of specifying the Invariant aspect with
the full declaration of the type instead of only at the declaration of the
partial view of the type. It's bizarre to have to make the invariant visible
to all clients; if often only relevant to the implementation of the type.
2) It would be useful if some mechanism existed for statically enforcing a
requirement that an invariant expression must not have side effects or, more
generally, must be "well behaved" (definition details TBD, but this might
include prohibitions on reading variables and/or on propagating exceptions).
3) It would be useful if the language made a distinction between "internal"
calls (where the caller is already inside the implementation of the type in
question) and "external" calls. No runtime invariant checking should be
performed for an "internal" call.
!proposal
(See wording.)
!wording
Modify 3.9.4(20.4/3):
otherwise, the action is the same as the action for the corresponding operation of
the parent type or progenitor type from which the operation was inherited
{except that additional invariant checks (see 7.3.2) and class-wide
postcondition checks (see 6.1.1) may apply)}. If there is more than one
such corresponding operation, the action is that for the operation that is not a
null procedure, if any; otherwise, the action is that of an arbitrary one of the
operations.
In 7.3.2(2/3), replace
Type_Invariant may be specified on a private_type_declaration or a
private_extension_declaration.
with
Type_Invariant may be specified on a private_type_declaration, on a
private_extension_declaration, or on a full_type_declaration that
declares the completion of a private type or private extension.
Add an AARM Note after 7.3.2(3/3):
Reason: A class-wide type invariant cannot be hidden in the private part, as
the creator of an extension needs to know about it in order to conform to it
in any new or overriding operations. On the other hand, a specific type
invariant is not inherited, so that no operation outside of the original
package needs to conform to it; thus there is no need for it to be visible.
Add before 7.3.2(7/3):
[Redundant: If the Type_Invariant aspect is specified for a type T,
then the invariant expression applies to T.]
Replace 7.3.2(9-16/3) by
* After successful default initialization of an object of type T,
the check is performed on the new object;
* After successful conversion to type T, the check is performed on
the result of the conversion;
* After assigning to a view conversion, outside the immediate scope
of T, that converts from T or one or more record extensions (and
no private extensions) of T to an ancestor of type T, a check is
performed on the part of the object that is of type T; similarly,
for passing a view conversion as an OUT or IN OUT parameter
outside the immediate scope of T, this check is performed upon
successful return;
* After a successful call on the Read or Input stream attribute of
the type T, the check is performed on the object initialized by
the stream attribute;
* Upon successful return from a call on any subprogram or entry that:
- is explicitly declared within the immediate scope of type T
(or by an instance of a generic unit, and the generic is
declared within the immediate scope of type T), and
- is visible outside the immediate scope of type T or overrides
an operation that is visible outside the immediate scope of T, and
- has a result with a part of type T, or one or more IN OUT or
OUT parameters with a part of type T, or an access to variable
parameter whose designated type has a part of type T.
the check is performed on each such part of type T.
Modify 7.3.2(17/3):
The invariant check consists of the evaluation of each invariant expression
that applies to T, on each of the objects specified above. If any of these
evaluate to False, Assertions.Assertion_Error is raised at the point of
the object initialization, conversion, or call. If a given call requires more
than one evaluation of an invariant expression, either for multiple objects
of a single type or for multiple types with invariants, [the order of ]the
evaluations {are performed in an arbitrary order}[is not specified],
and if one of them evaluates to False, it
is not specified whether the others are evaluated. Any invariant check is
performed prior to copying back any by-copy in out or out parameters.
{Invariant checks, any postcondition check, and any constraint checks associated
with by-copy in out or out parameters are performed in an arbitrary order.}
[It is not specified whether any constraint checks associated with by-copy in
out or out parameters are performed before or after any invariant checks. It is
not specified whether any postcondition checks are performed before or after any
invariant checks.]
Replace 7.3.2(18/3) by:
The invariant checks performed on a call are determined by the subprogram or
entry actually invoked, whether directly, as part of a dispatching call, or as
part of a call through an access-to-subprogram value.
Add after 7.3.2(19/3):
Note: A call of a primitive subprogram of type NT that is inherited from type T
needs to satisfy the specific invariants of both the types NT and T. A call
of a primitive subprogram of type NT that is overridden for type NT needs to
satisfy only the specific invariants of type NT.
!discussion
Item (1) is addressed in the wording proposal above.
For item (2), it seems premature to define such restrictions. Implementations
can define their own; and we'll revisit this next time.
For item (3), the language does make such a distinction, but it
makes it between subprograms, not calls. Subprograms declared in the visible
part are external, others are internal. This also seems right: A called
subprogram doesn't know who is its caller, so if it is externally callable, it
needs to ensure the invariant is true on return. This seems right, so no
change is needed now.
The change to 7.3.2(17/3) is to use the "arbitrary order" wording used by the
rest of the standard.
The remaining changes are to clarify when checks are and are not performed, and
to fix holes caused by view conversions.
!corrigendum 3.9.2(20.2/2)
Replace the paragraph:
Force a conflict; the real text is found in the conflict file.
by:
Nothing interesting.
!corrigendum 7.3.2(0)
Insert new clause:
Force a conflict; the real text is found in the conflict file.
!ACATS test
Create ACATS C-Tests to ensure that the invariant checks are made in all of
the defined cases.
!ASIS
No ASIS impact (beyond the original AI).
!appendix
From: Steve Baird
Sent: Wednesday, June 15, 2011 4:24 PM
An AdaCore customer has identified three issues with Ada 2012's type invariants. I'm passing these along so that the ARG can decide for each whether
a) some action is needed for Ada 2012; or
b) some action is needed, but not for Ada 2012; or
c) no action is needed.
====
1) It would be useful to have the option of specifying the Invariant aspect with
the full declaration of the type instead of only at the declaration of the
partial view of the type.
If what the user really wants is
package Pkg is
type Stack is private;
<exported operations on type T>
private
type Stack is record
Max, Current : Index := 0;
...;
end record with Invariant => Stack.Current <= Stack.Max;
end Pkg;
, it is annoying to have to write
package Pkg is
type Stack is private with Invariant => Is_Valid (T);
<exported operations on type T>
function Is_Valid (X : Stack) return Boolean;
private
type Stack is record
Max, Current : Index:= 0;
...;
end record;
function Is_Valid (X : T) return Boolean is
(X.Current <= X.Max);
end Pkg;
, thereby adding an unwanted visible operation (Is_Valid) to the interface. If a
user chooses to think of the invariant as an implementation detail, not part of
the public interface (and not part of a contract which clients need to be aware
of), then that user doesn't want to see any mention of the invariant in the
visible part.
Introducing the Is_Valid function (albeit a function whose completion is an
expression_function) may also have interactions with issue #2 (below).
====
2) It would be useful if some mechanism existed for statically enforcing a
requirement that an invariant expression must not have side effects or, more
generally, must be "well behaved" (definition details TBD, but this might
include prohibitions on reading variables and/or on propagating exceptions).
A new language-defined restriction which only allows "well behaved" invariant
expressions could address this issue.
Concern was also expressed about the particular case of an invariant expression
whose evaluation leads to infinite recursion because the expression itself
contains some construct whose evaluation requires evaluation of the invariant
expression (e.g., due to a type conversion or to a call to a function with an
out-mode parameter).
Hopefully the as-yet-uninvented restriction would catch this case.
====
3) It would be useful if the language made a distinction between "internal"
calls (where the caller is already inside the implementation of the type in
question) and "external" calls. No runtime invariant checking should be
performed for an "internal" call.
The concern here is correctness, not performance.
Inside the implementation, it is perfectly reasonable to
(temporarily) violate a type's invariant. An invariant check performed while
"the hood is up" can be a problem.
One (partial) workaround is to implement each exported operation Foo as a rename
of a non-exported Foo_Implementation subprogram. "Internal" callers who want to
call Foo then call Foo_Implementation instead. Or the private type in question
could be implemented as a derived type with invariant-breaking operations
performed using the non-exported parent type and then only converting to the
exported type when the invariant has been restored.
Either of these approaches is cumbersome.
=====
My own opinions:
#1 I can see the argument for this. I would not
be opposed to allowing the Invariant spec to
be supplied as part of either the private
type declaration (as it is today) or the
completion.
#2 Defining a new restriction for folks who want
more restrictions on invariant expressions
seems reasonable, but lots of details TBD.
#3 The AI currently says
The invariant checks performed on a call are determined by the
subprogram or entry actually invoked, whether directly, as
part of a dispatching call, or as part of a call through an
access-to-subprogram value.
There are good reasons for this rule and I think messing with
it would lead to problems.
****************************************************************
From: Randy Brukardt
Sent: Wednesday, June 15, 2011 5:00 PM
...
> #2 Defining a new restriction for folks who want
> more restrictions on invariant expressions
> seems reasonable, but lots of details TBD.
Such a restriction makes perfect sense, and should apply to all contracts (that
is, preconditions, postconditions, and subtype predicates) but in the past when
I've proposed such things I've not gotten any traction. I suspect that this is
an area where an implementer needs to take the lead (I definitely will do
something on this like in Janus/Ada should I ever get to implementing contracts,
but obviously something AdaCore does will have a lot more impact).
****************************************************************
From: Edmond Schonberg
Sent: Wednesday, June 15, 2011 5:10 PM
> ...
>> #2 Defining a new restriction for folks who want
>> more restrictions on invariant expressions
>> seems reasonable, but lots of details TBD.
>
> Such a restriction makes perfect sense, and should apply to all
> contracts (that is, preconditions, postconditions, and subtype
> predicates) but in the past when I've proposed such things I've not
> gotten any traction. I suspect that this is an area where an
> implementer needs to take the lead (I definitely will do something on
> this like in Janus/Ada should I ever get to implementing contracts,
> but obviously something AdaCore does will have a lot more impact).
There have been several user suggestions along those lines, so we will
definitely introduce such a restriction. Implementation seems straightforward
if the definition is tight enough. Should there be a pragma (sorry, an aspect)
that asserts that the body of a function satisfies this restriction? They seem
to go together.
****************************************************************
From: Randy Brukardt
Sent: Wednesday, June 15, 2011 6:17 PM
> > ...
> >> #2 Defining a new restriction for folks who want
> >> more restrictions on invariant expressions
> >> seems reasonable, but lots of details TBD.
> >
> > Such a restriction makes perfect sense, and should apply to all
> > contracts (that is, preconditions, postconditions, and subtype
> > predicates) but in the past when I've proposed such things I've not
> > gotten any traction. I suspect that this is an area where an
> > implementer needs to take the lead (I definitely will do something
> > on this like in Janus/Ada should I ever get to implementing
> > contracts, but obviously something AdaCore does will have a lot more impact).
>
> There have been several user suggestions along those lines, so we
> will definitely introduce such a restriction.
> Implementation seems straightforward if the definition is tight
> enough. Should there be a pragma (sorry, an aspect) that asserts that
> the body of a function satisfies this restriction? They seem to go
> together.
Yes, I think that is required in order to support separate compilation (and
dispatching, in class-wide contracts). The question of course is whether this
enforces restrictions on the body, and what those restrictions are in that case.
This was one of the purposes of the global in/global out annotations, after all:
a restriction on the global in/global out allowed in functions called from
contract expressions would be easy to specify and enforce. But of course that
depends on the full global in/global out mechanisms. Something more limited in
scope would be easier to define, inplement, and most likely use.
In any case, something to talk about at the meeting. Probably best as a post-Ada
2012 feature, but something that we can scope out anytime as implementations can
add their own aspects and restrictions (so there is no pressing rush).
****************************************************************
From: Randy Brukardt
Sent: Wednesday, June 15, 2011 6:21 PM
...
> #3 The AI currently says
> The invariant checks performed on a call are determined by the
> subprogram or entry actually invoked, whether directly, as
> part of a dispatching call, or as part of a call through an
> access-to-subprogram value.
>
> There are good reasons for this rule and I think messing with
> it would lead to problems.
Right. Keep in mind that AI05-0247-1 modifies these rules slightly, to ensure
that inherited routines enforce all of the invariants (including ones the
original body does not know about).
In any case, I'll make a skeleton AI to hold this mail so we have something to
discuss at the meeting next week.
****************************************************************
From: Tucker Taft
Sent: Wednesday, June 15, 2011 8:37 PM
It certainly makes perfect sense to make the Invariant private, since it is
really something to support the implementation, not the client.
As far as restrictions, that seems not worth standardizing at this point, and I
would expect good compilers to provide warnings without any effort on the part
of the user if the invariant has side-effects or other weirdness.
Distinguishing internal from external calls seems to be more trouble than it is
worth. The called subprogram doesn't know who is its caller, so if it is
externally callable, it pretty much needs to ensure the invariant is true on
return. Inlining can be a way of dealing with this without any extra language
support, for the unusual case where it is needed.
****************************************************************
From: Robert Dewar
Sent: Thursday, June 16, 2011 4:39 AM
...
> As far as restrictions, that seems not worth standardizing at this
> point, and I would expect good compilers to provide warnings without
> any effort on the part of the user if the invariant has side-effects
> or other weirdness.
I agree, let implementations respond to actual usage and suggestions and needs
of users, standardize next time around if appropriate.
****************************************************************
From: Yannick Moy
Sent: Thursday, June 16, 2011 2:42 AM
> 3) It would be useful if the language made a distinction between
> "internal" calls (where the caller is already inside the
> implementation of the type in question) and "external" calls. No
> runtime invariant checking should be performed for an "internal" call.
Indeed, this is what the customer initially suggested, based on his experience
with Eiffel and C++:
- In Eiffel, it is the syntactic difference between a qualified call "a.f(...)"
and an unqualified call "f(...)" (called from a method on the implicit
"Current") that decides whether the invariant is checked or not. It is not
checked at all on unqualified calls. It is checked on both entry and exit from
qualified calls.
- For C++, the customer developed their own implementation of C++ macros which
implement almost fully the rules of design by contract:
- during evaluation of assertions, the function is executed without evaluation
of the associated assertions (valid for all assertions)
- during an internal call, the invariant is not assessed.
The distinction between internal and external calls is implemented with a simple
imbrication counter in the implicit attributes of all objects: if the
imbrication counter is > 1 during a call, the invariant is not evaluated.
But in the conversation that follows, I explained that the distinction between
internal and external *calls* is not appropriate. Rather, we should distinguish
internal and external *subprograms*. What I mean is the following. Suppose you
want to verify formally code that respects the policy of Eiffel. So every
routine over type T can be called either in a context in which the invariant of
T holds, in which case it must reestablish the invariant at the end, or in a
context in which the invariant of T does not hold. This means that every routine
has really *two* different contracts... well, not really. Some routines will be
called only in a context in which the invariant holds, and they may rely on
this, so that they do not execute properly if called in a context in which the
invariant does not hold. So in the end you don't know really whether a routine
should work only in a context in which the invariant holds, or always.
If you perform runtime checking, that's not a problem, because the dynamic
environment tells you in which case you are. But if you aim at formal
verification, you are left with no other choice than ask the user to provide
this information. Since we aim at both with Ada 2012, I much prefer a rule which
states exactly which routines expect to be called in a context in which the
invariant holds. We agreed that such a rule is to check invariants only on
public operations of a type, not on private subprograms (either declared in
private part or in body). So that's this rule that I would like the ARG to
consider.
On 16/06/2011 03:36, Tucker Taft wrote:
> Distinguishing internal from external calls seems to be more trouble
> than it is worth. The called subprogram doesn't know who is its
> caller, so if it is externally callable, it pretty much needs to
> ensure the invariant is true on return. Inlining can be a way of
> dealing with this without any extra language support, for the unusual
> case where it is needed.
As explained above, this issue is rather external vs. internal *subprograms*.
Without this distinction, the customer says invariants are "unusable" in his
context. Note that this customer uses pre- and postconditions (pragmas)
extensively (AdaCore developed these for them). My experience is that languages
that do not have a distinction of this kind lead to unusable invariants:
- in Spec# (C#), it is the user responsibility to "open" and "close" objects,
with the invariant being checked on entry/exit of a call only when the caller
object is "closed". Very heavy.
- in JML (Java), the invariant is required to hold on entry/exit of every call.
As a result, invariants are almost not used; people prefer using pre- and
postconditions.
What would be the problem with this (simple) rule enforcing invariant only on
external subprograms?
****************************************************************
From: Yannick Moy
Sent: Thursday, June 16, 2011 8:34 AM
> As explained above, this issue is rather external vs. internal *subprograms*.
Our customer pointed us today to the following sentence in B. Meyer's book
"Object-Oriented Software Construction 2nd edition", p 366 under "Who must
preserve the invariant?":
"As a consequence, the obligation to maintain the invariant applies only to the
body of features that are exported either generally or selectively; a secret
feature - one that is available to no client - is not affected by the
invariant."
So Eiffel already has this policy of checking the invariant only on external
*subprograms*, plus it has the internal/external *call* difference. I believe
Ada could implement only the first one, and it would be enough to satisfy the
needs expressed so far.
Ideally, a renaming-as-body of a private operation into a public one would add
the verification of the invariant if necessary:
spec:
type T is ... with Invariant => Inv(T);
procedure External (X : out T); -- Inv(X) checked on exit
body:
procedure Internal (X : out T); -- no invariant checking
procedure External (X : out T) renames Internal; -- adds Inv(X) checking
which would give an easy way to use an operation both externally (with invariant
checked) and internally (no check).
****************************************************************
From: Randy Brukardt
Sent: Thursday, June 16, 2011 12:08 PM
...
> What would be the problem with this (simple) rule enforcing invariant
> only on external subprograms?
There is no problem -- it is ALREADY the rule for Type_Invariants in Ada 2012.
Specifically, 7.3.2(12-5/3) [the number is from the working draft of the
Standard, not sure what it was in Draft 11] says about when an invariant is
checked:
Upon return from a call on any subprogram or entry that:
* has a result of type T, or one or more in out or out parameters of type
T,
* is explicitly declared within the immediate scope of type T (or is a part
of an instance of a generic unit declared within the immediate scope of
type T), and
* is visible outside the immediate scope of type T or overrides an
operation that is visible outside the immediate scope of T,
Note that the last part requires the routine to be one that is visible to
clients; it excludes private operations unless they are overriding some visible
inherited routine.
So the rule you are suggesting is in fact the rule Ada 2012 requires. If your
description of the problem is correct, then we need to do nothing. (Whether GNAT
properly implements these rules is another question, but irrelevant to the ARG.)
****************************************************************
From: Tucker Taft
Sent: Thursday, June 16, 2011 4:34 PM
> ... What would be the problem with this (simple) rule enforcing
> invariant only on external subprograms?
As Randy pointed out, this is exactly what Ada 2012 does.
****************************************************************
From: Randy Brukardt
Sent: Thursday, June 16, 2011 6:54 PM
But thanks for confirming that we have it right already. It's one less thing to
worry about. :-)
****************************************************************
From: Randy Brukardt
Sent: Thursday, June 16, 2011 7:05 PM
...
> As far as restrictions, that seems not worth standardizing at this
> point, and I would expect good compilers to provide warnings without
> any effort on the part of the user if the invariant has side-effects
> or other weirdness.
Well, I surely agree that it is too late for any such restrictions in Ada 2012.
But I don't think it is practical to produce warnings for "bad" contract
expressions; you could only catch some low-hanging fruit and I have to wonder if
such warnings would actually be harmful (by giving a false sense of security).
But such warnings aren't possible if the "bad" things occur within called
functions; expression functions help a bit, but can provide no help for
class-wide contracts as the calls are all dispatching. And as Bob has repeatedly
noted, banning all functions other than expression functions and predefined
operators really isn't practical (especially in the class-wide cases). We really
need some sort of function categorization aspect (or global in/global out
aspects), and that would work with the warnings and/or restrictions to fully
cover the needs.
I do expect AdaCore to end up taking the lead on this, because they clearly have
customer requests for this functionality and they will need to convince the
entire ARG of what is needed (as I have). That's both good and bad (good because
something will actually get done here, bad because the result is likely to be
whatever is easiest for GNAT rather than technically best), but I don't think it
can be helped.
****************************************************************
From: Yannick Moy
Sent: Friday, June 17, 2011 2:01 AM
>>> ... What would be the problem with this (simple) rule enforcing
>>> invariant only on external subprograms?
>
>> As Randy pointed out, this is exactly what Ada 2012 does.
>
> But thanks for confirming that we have it right already. It's one less
> thing to worry about. :-)
thanks for the good news that I'll transmit with pleasure to our customer!
****************************************************************
From: Steve Baird
Sent: Monday, June 20, 2011 2:32 PM
>> It would be useful to have the option of specifying the Invariant
>> aspect with the full declaration of the type instead of only at the
>> declaration of the partial view of the type.
> It certainly makes perfect sense to make the Invariant private, since
> it is really something to support the implementation, not the client.
There seems to be general support for this idea.
Just so that we have a concrete proposal to discuss (whether in Edinburgh or
later), here is a proposed wording change.
====
!wording
In 7.3.2(2/3), replace
Type_Invariant may be specified on a private_type_declaration or a
private_extension_declaration.
with
Type_Invariant may be specified on a private_type_declaration, on a
private_extension_declaration, or on a full_type_declaration which
declares the completion of a private type or private extension.
In 7.3.2(3/3), replace
Type_Invariant'Class may be specified on a private_type_declaration
or a private_extension_declaration.
with
Type_Invariant'Class may be specified on a private_type_declaration,
on a private_extension_declaration, or on a full_type_declaration
which declares the completion of a private type or private extension.
****************************************************************
From: Erhard Ploedereder
Sent: Saturday, June 25, 2011 3:35 AM
This is how I understand the most recently proposed principles:
Within the full view of a type, its class-invariants are not checked.
Reason: As plain assigments to visible components could violate the invariants
without any checking preventing it, it makes no sense to check invariants, if
said changes are effected by calls on some subprograms.
Within a partial view of the declared type of a variable, all
(redundant: dispatching or non-dispatching) calls on primitive operations of
this type with the variable as controlling/first argument check all
class-invariants of the actual type of the object denoted by the variable. (In
addition, any non-class invariant is checked - presumably the one that matches
the view for the call.)
Reason: It should be guaranteed that despite potential up-casts (i.e., view
conversions) and even in the presence of statically bound calls, the invariants
of the object cannot be violated by the completed call.
-------------------------
Other questions (which may or may not be answered already by the RM:
Are invariants and post-conditions checked when the call completes with an
exception? Presumably not, but where does it say that?
Why aren't invariants checked upon entry as well? They are supposed to hold
there, too. For types that have visible components this would make a lot of
sense. For fully private types, they are guaranteed by the last call.
How do class-wide operations play here?
****************************************************************
From: Erhard Ploedereder
Sent: Saturday, June 25, 2011 6:44 AM
This is how I understand the most recently proposed principles ( further amended
to make them work reasonably):
Within the full view of a type, its class-invariants are not checked.
Reason: As plain assigments to visible components could violate the invariants
without any checking preventing it, it makes no sense to check invariants, if
said changes are effected by calls on some subprograms instead.
(Possible variation, if deemed easier to implement or safer: the
class-invariants of the static view of the subprogram are checked.)
Within a partial view of a type, all (redundant: dispatching or non-dispatching)
calls on subprograms whose body has a full view of this type and has an actual
parameter of the type check all class-invariants of the actual type of the
object denoted by the parameter. Multiple such parameters cause multiple such
checks. (In addition, any non-class invariant is checked - presumably the one
that comes with the body of the subprogram, whichever it might be.)
Reason: It should be guaranteed that despite potential up-casts and even in the
presence of statically bound calls, the invariants of the type of the !object!
cannot be violated by the completed call.
-------------------------
Other questions (which may or may not be answered already by the RM:
Are invariants and post-conditions checked when the call completes with an
exception? Presumably not, but where does it say that?
Why aren't invariants checked upon entry as well? They are supposed to hold
there, too. For types that have visible components this would make a lot of
sense. For fully private types, they are guaranteed by the last call and hence
could be optimized away.
When can the checks be optimized away? (even in the presence of
unchecked_* stuff?)
(How do class-wide operations play? They are included in the above, as are any
other subprograms that have visibility to the type's details.)
****************************************************************
From: Tucker Taft
Sent: Saturday, June 25, 2011 10:26 AM
Replace the 7.3.2(10-16/3) with:
Static Semantics
[Redundant: If the Type_Invariant aspect is specified for a type T,
then the invariant expression applies to T.]
[Redundant: If the Type_Invariant'Class aspect is specified for a tagged type
T, then the invariant expression applies to all descendants of T.]
Dynamic Semantics
If one or more invariant expressions apply to a type T, and the
Assertion_Policy (see 11.4.2) at the point of the partial view declaration for
T is Check, then an invariant check is performed at the following places, on
the specified object(s):
* After successful default initialization of an object of type T,
the check is performed on the new object;
* After successful conversion to type T, the check is performed on
the result of the conversion;
* After assigning to a view conversion, outside the immediate scope
of T, that converts from T or one or more record extensions (and
no private extensions) of T to an ancestor of type T, a check is
performed on the part of the object that is of type T; similarly,
for passing a view conversion as an OUT or IN OUT parameter
outside the immediate scope of T, this check is performed upon
successful return;
* After a successful call on the Read or Input stream attribute of
the type T, the check is performed on the object initialized by
the stream attribute;
* Upon successful return from a call on any subprogram or entry that:
- is explicitly declared within the immediate scope of type T
(or is a part of an instance of a generic unit declared within
the immediate scope of type T), and
- is visible outside the immediate scope of type T or overrides
an operation that is visible outside the immediate scope of T,
- has a result with a part of type T, or one or more IN OUT or
OUT parameters with a part of type T, or an access to variable
parameter whose designated type has a part of type T.
the check is performed on each such part of type T.
****************************************************************
From: Randy Brukardt
Sent: Sunday, June 26, 2011 4:25 AM
Modify 3.9.2(20.4):
otherwise, the action is the same as the action for the corresponding operation
of the parent type or progenitor type from which the operation was inherited
{except that additional invariant checks (see 7.3.2) and class-wide
postcondition checks (see 6.1.1) may apply}. If there is more than one such
corresponding operation, the action is that for the operation that is not a null
procedure, if any; otherwise, the action is that of an arbitrary one of the
operations.
Delete 7.3.2(18/3).
****************************************************************
From: Erhard Ploedereder
Sent: Sunday, June 26, 2011 4:51 AM
Proposed Wording:
Note: A call on a primitive subprogram of type NT that is inherited from type T
will need to satisfy the specific invariants of both the types NT and T. A call
on a primitive subprogram of type NT that is redefined for type NT will need to
satisfy only the specific invariants of the type NT.
****************************************************************
From: Yannick Moy
Sent: Monday, June 27, 2011 1:54 AM
> Other questions (which may or may not be answered already by the RM:
>
> Are invariants and post-conditions checked when the call completes
> with an exception? Presumably not, but where does it say that?
I guess that's the meaning of "successful return" in:
* Upon successful return from a call on any subprogram or entry that: [...]
> Why aren't invariants checked upon entry as well? They are supposed to
> hold there, too. For types that have visible components this would
> make a lot of sense. For fully private types, they are guaranteed by
> the last call.
AI says:
> The invariant checks are performed as postcondition checks to ensure
> that violations are caught as soon as possible. Presumably the
> invariants could also be enforced as preconditions, but those checks
> would in general be redundant, and the failures would be harder to
> track down since the call that actually created the problem would be
> harder to identify.
I would add as an important benefit that invariant is not checked at all on
calls to functions taking only IN parameters. This is crucial to be able to have
calls to (public) functions or expression functions in invariants. Otherwise
you'd get an infinite loop.
****************************************************************
From: Yannick Moy
Sent: Monday, June 27, 2011 2:02 AM
The AI wording you sent does not contain the proposed amendment sent by Steve on
2011/06/20, to allow invariants being defined on full_type_declaration for a
private type. (with the possibility of direct component access in the invariant)
Does that mean this amendment was not adopted?
BTW, the example in !proposal should mention Type_Invariant, not Invariant.
****************************************************************
From: Randy Brukardt
Sent: Thursday, June 30, 2011 2:33 PM
...
> The AI wording you sent does not contain the proposed amendment sent
> by Steve on 2011/06/20, to allow invariants being defined on
> full_type_declaration for a private type.
> (with the possibility of direct component access in the invariant)
>
> Does that mean this amendment was not adopted?
No, it means that Tuck started with an obsolete AI rather than the current
wording of the Standard as amended by the first day of the meeting.
It will be the editor's job (that is, me) to merge all of the various decisions
into a single whole.
In this case, there was some concern about whether Type_Invariant'Class should
be required to be visible (because it affects child types), while there is no
reason for specific Type_Invariants to be visible. Deciding that was deferred,
and I'm not sure that we ever actually decided that (I didn't see a decision in
a quick scan of my notes).
We ought to do that. ;-)
****************************************************************
From: Randy Brukardt
Sent: Wednesday, July 27, 2011 9:36 PM
Actually, after reading my notes carefully, what happened is that we immediately
decided to adopt Steve's wording of June 20th (changing "which" to "that") for
Type_Invariant only (not Type_Invariant'Class, since descendants need to know
about it in order to write operations correctly). That happened in the first 30
minutes of the meeting.
We then spent the entire remainder of the 3 day meeting changing type invariants
(doing other things in between discussions), not concluding until there was 30
minutes left in the meeting. By then, we'd totally forgotten about the initial
decision.
I'm going to presume that we still intend this change (I can't think of any
reason why not), so anyone that disagrees should speak up.
P.S. I didn't actually explain the change:
In 7.3.2(2/3), replace
Type_Invariant may be specified on a private_type_declaration or a
private_extension_declaration.
with
Type_Invariant may be specified on a private_type_declaration, on a
private_extension_declaration, or on a full_type_declaration that
declares the completion of a private type or private extension.
****************************************************************
From: Bob Duff
Sent: Friday, July 1, 2011 8:17 AM
> !standard 7.3.2 (00) 10-10-19 AI05-0146-1/08
This AI is inconsistent about the name of the aspect -- Invariant versus
Type_Invariant. IMHO it should be Invariant, because "Type_" is just noise --
you can see from the syntax that it applies to the type it's attached to.
If we had package invariants, they should be called Invariant, too, not
Package_Invariant.
****************************************************************
From: Randy Brukardt
Sent: Friday, July 1, 2011 6:54 PM
> > !standard 7.3.2 (00)
> 10-10-19 AI05-0146-1/08
>
> This AI is inconsistent about the name of the aspect -- Invariant
> versus Type_Invariant.
No, it's not. The !wording consistently uses Type_Invariant. The examples are
just plain wrong, and all that means is that someone forgot to update them. Big
deal.
In any case, this AI is not going to be changed, because it is already WG 9
approved. AI05-0250-1 will include the changes we approved at the meeting.
> IMHO it should be
> Invariant, because "Type_" is just noise -- you can see from the
> syntax that it applies to the type it's attached to.
Huh? We use exactly the same syntax for subtype predicates. They don't apply to
the type, only the subtype.
The whole point of saying "Type_Invariant" is to make it clear that this is
type-related, as opposed to predicates, which are subtype-related. These use the
same syntax and are allowed on some of the same declarations (and conceivably
could be used at the same time on a declaration). Recall that the name of the
predicates was "Subtype_Predicate" before we split them into static and dynamic
versions -- these really should be Static_Subtype_Predicate and
Dynamic_Subtype_Predicate, but those are too long. There was a lot of confusion
about the difference between these two, and we wanted to make it crystal clear
which was which. That need has not gone away (even if the ARG itself is more
comfortable with the distinction).
In any case, we just spent 1/3 of the recent meeting talking about "type
invariants", and that would have been the perfect time to raise this issue. I
have to assume you really don't feel that strongly about it or you would have
had to say something! It's now effectively too late, in that with the holidays
and summer vacations, it will be impossible to have a discussion with everyone
involved. (And e-mail discussions tend to be dominated by a handful of people.)
And quite frankly, naming discussions are interminable and a bad use of my (and
everyone else's) limited time. (30 messages = 1 hour of my time on average.)
> If we had package invariants, they should be called Invariant, too,
> not Package_Invariant.
Perhaps, but there is no possibility of confusion there (there isn't any such
thing as a subpackage). And in any case, we don't have package invariants and
are unlikely to ever have them (the semantic problems aren't suddenly going to
disappear at some point in the next 5 years), so what they might be called seems
irrelevant.
****************************************************************
From: Bob Duff
Sent: Friday, July 1, 2011 5:54 AM
>...(30 messages = 1
> hour of my time on average.)
That's an interesting statistic. I get about 300 emails per day, mostly on
report@adacore.com. (That's week days; I think it's less than 100 on weekend
days.) So if I spent 1 hour per 30, I'd spend 10 hours a day doing nothing but
reading and filing email. Yikes!
****************************************************************
From: John Barnes
Sent: Saturday, July 2, 2011 9:50 AM
And the Rat says Type_Invariant, so that's that.
****************************************************************
From: Bob Duff
Sent: Saturday, July 2, 2011 11:30 AM
Hmm, this could save Randy and the rest of us a lot of trouble. Let's just go
by what's in the Rat, and forget about this silly RM document.
****************************************************************
Questions? Ask the ACAA Technical Agent