Version 1.5 of ai05s/ai05-0146-1.txt
!standard 11.5 (00) 09-11-02 AI05-0146-1/03
!standard 11.4.1 (10)
!class amendment 09-02-15
!status work item 09-02-15
!status received 09-02-15
!priority Medium
!difficulty Medium
!subject Type and Package Invariants
!summary
To augment the basic "assert" pragma capability of Ada 2005,
we propose constructs for specifying invariants for types.
The semantics for these constructs are defined in terms of the
Assertion_Error exception used by the Assert pragma and the
Assertion_Policy configuration pragma.
!problem
A number of programming paradigms include the heavy use of invariants
associated with types or modules (i.e. packages). Having a basic
standardized "Assert" pragma supports this approach to some degree, but
generally requires that the Assert pragmas actually be inserted inside the
bodies of the associated code. It would be much more appropriate if these
invariants appeared on the specification of the types and packages rather
than buried in the body, as it really represents part of the contract. In
particular, one wants any implementation of a given package spec to conform
to all of invariants specified, in the same way one wants any
implementation of a package to conform to the constraints of the parameter
and result subtypes of the visible subprograms of the package.
Note that type invariants are not the same thing as constraints, as
invariants apply to all values of a type, while constraints are
generally used to identify a subset of the values of a type. Invariants
are only meaningful on private types, where there is a clear boundary
(the enclosing package) that separates where the invariant applies
(outside) and where it need not be satisfied (inside). In some ways, an
invariant is more like the range of values specified when declaring a
new integer type, as opposed to the constraint specified when defining
an integer subtype. The specified range of an integer type can be
violated (to some degree) in the middle of an arithmetic computation,
but must be satisfied by the time the value is stored back into an
object of the type.
Invariants can help to more accurately define the "contract" between the
user and implementor of a package, and thereby to catch errors in usage
or implementation earlier in the development cycle. They also can
provide valuable documentation of the intended semantics of an
abstraction.
!proposal
We propose to allow the specification of an Invariant "aspect" of a
type, as well as an Invariant'Class aspect of a tagged type. These
aspects are specified using a construct of the following form:
package Q is
type T(...) is private
with Invariant => Is_Valid(T);
type T2(...) is abstract tagged private
with Invariant'Class => Is_Valid(T2);
function Is_Valid(X : T) return Boolean;
function Is_Valid(X2 : T2) return Boolean is abstract;
end Q;
The invariant expression associated with a type is evaluated as a postcondition
of any operation that creates, updates, or returns a value of the type.
!wording
Modify 7.3(2 and 3/2):
private_type_declaration ::=
type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private
[aspect_specification];
private_extension_declaration ::=
type defining_identifier [discriminant_part] is
[abstract] [limited | synchronized] new ancestor_subtype_indication
[and interface_list] with private
[aspect_specification];
Add new section:
13.3.3 Type Invariants
An invariant for a private type or private extension may be specified
using an aspect_specification for the aspect Invariant and, if tagged,
for the aspect Invariant'Class. The associated expression is called
an invariant expression.
Name Resolution
The expected type for an invariant expression is the predefined type
Boolean. [Redundant: Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
of the type.] Within an invariant expression associated with type T,
the type of the current instance is T for the Invariant aspect and
T'Class for the Invariant'Class aspect.
Legality Rules
[Redundant: The Invariant'Class aspect shall not be specified for an
untagged type.] The Invariant aspect shall not be specified for an
abstract type.
Static Semantics
[Redundant: If the 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
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 default initialization of an object of type T, on the new object;
* After conversion to type T, on the result of the conversion;
* 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, and
- is visible outside the immediate scope of type T, overrides
an operation that is visible outside the immediate scope of T,
or has its Access attribute evaluated;
on the result object of type T, and on each IN OUT or OUT
actual parameter of type T.
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, Ada.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 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. 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.
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.
[Redundant: If the Assertion_Policy in effect at the point of a
subprogram or entry declaration is Ignore, then no invariant check is
performed on a call on that subprogram or entry.]
!discussion
We have provided only type oriented "invariant"
specifications. We considered but ultimately rejected the idea of
package-oriented invariants (see section on this below).
For type invariants, we apply them on [IN] OUT parameters of procedures
after the call, and on the result of functions, conversions, and default
initializations.
The type invariants are defined by a boolean expression, with any
appearance of the type name within the expression treated as a reference
to the "current instance," which is the value being checked against the
invariant. We considered allowing only the name of a boolean function,
but the more general boolean_expression was felt to be useful at least
in same cases.
For type invariants, name resolution on the boolean expression is not
performed until reaching the end of the visible part of the enclosing
package, which is clearly necessary given the placement of the
aspect specification on the declaration of the partial view.
Invariant checks apply to all calls on (relevant) subprograms declared in
the visible part of the package, even for calls from within the package.
This allows the checks to be performed inside the procedures rather than
at the call point, and makes the invariants equivalent to a
series of postconditions. We considered making invariant checks
apply only to calls from outside the package, but this appeared to
complicate the implementation and description with little additional
benefit.
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.
We have adopted a rule that the invariant checks performed are determined
by the subprogram invoked, whether directly or indirectly, to match
the rule for pre- and postconditions. Note that we assume that any
subprogram that has its Access attribute evaluated might be called from
outside the package.
Assertion Policy
We have used the Assertion_Policy pragma defined in Ada 2005,
with the same options and interpretation. It might make sense
to define a separate pragma, such as Invariant_Policy, but with the
same set of identifiers. This would give the programmer more
control. On the other hand, typically either the programmer wants
full debugging, or full speed. Intermediate points seem relatively
rare, and it seems even more unlikely that the intermediate point
would correspond to the distinction between assertions and
invariants.
Package Invariants not provided
We considered providing package invariants. This reflected the fact
that some abstractions are for abstract data types, where type-oriented
invariants make sense, while others are for abstract state machines,
where a package-oriented invariant would make sense. Here is the part of
the original proposal associated with them, for historical reference.
We decided there was not a particularly good syntax for specifying them,
and they didn't seem to add sufficient benefit over simply using
postconditions.
This was the general form of a package invariant:
package P is
pragma Invariant(P, Validate);
...
function Validate return Boolean;
end P;
Here is a more formal syntax for the pragma:
pragma Invariant(package_local_name,
[Check =>] boolean_expression [, [Message =>] string_expression]);
The package_local_name for pragma Invariant must denote the immediately
enclosing program unit, which must be a package.
Checks would be performed as follows:
* For a package Invariant pragma, upon return
from a call on any procedure defined within the declarative
region of the package that is visible outside the package,
a check is made that the given boolean_expression evaluates to True;
also, immediately after completing elaboration of the package.
We would propose the same name resolution deferral for package
invariants, though there it is less critical, presuming we stick with a
pragma. If we were to use something like the aspect specification
syntax for a package invariant (e.g. "package P with Invariant =>
Validate is ... end P;") then we would clearly have to defer name
resolution.
We would only enforce the package-oriented invariant on return from
visible procedures of the package. If a visible function has
side-effects, the implementor may want to insert an explicit
postcondition on the function, or an Assert pragma inside.
!example
generic
type Item is private;
package Stacks is
type Stack is private
with Invariant => Is_Valid_Stack(Stack);
function Is_Empty(S : in Stack) return Boolean;
function Is_Full(S : in Stack) return Boolean;
procedure Push(S : in out Stack; I : in Item)
with Pre => not Is_Full(S)
Post => not Is_Empty(S);
procedure Pop(S : in out Stack; I : out Item)
with Pre => not Is_Empty(S)
Post => not Is_Full(S);
function Top(S : in Stack) return Item
with Pre => not Is_Empty(S);
function Is_Valid_Stack(S : in Stack) return Boolean;
Stack_Error : exception;
private
--
end Stacks;
!ACATS test
!appendix
From: Tucker Taft
Sent: Sunday, February 15, 2009 4:30 PM
Here is a resurrection of AI95-00375 on type and package invariants.
We discussed the type invariants at AdaCore. I left in the
Package_Invariant because it seemed simple and useful.
[This is version /01 of the AI - ED.]
****************************************************************
From: Bob Duff
Sent: Tuesday, February 24, 2009 10:25 AM
[Find the message that this is replying to in AI05-0145-1.]
> type Set is interface
> with
> Invariant'Class =>
> (Is_Empty(X)) = (Count(X) = 0);
I think invariants should apply to subtypes, not just types.
I think they are like constraints, and at least for scalars, can be checked in
the same places.
****************************************************************
From: Gary Dismukes
Sent: Thursday, February 26, 2009 12:09 AM
Randy brought up that point at the meeting and he has an action item to make a
specific proposal along those lines.
****************************************************************
From: Robert Dewar
Sent: Thursday, February 26, 2009 12:09 AM
I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and
think that pre/post conditions are important enough to warrant syntax additions.
I do think that postconditions in the body are useful, and so would keep the
pragmas, certainly in GNAT anyway. It is true that preconditions in the body
are just assertions, so they are there just for symmetry, but postconditions
in the body are useful in that they come up front, which is the right position,
and they block all exits (which would be tedious to do manually with assertions).
I also think it is good to be able to control pre/post conditions separately
from normal assertions.
****************************************************************
From: Alan Burns
Sent: Thursday, February 26, 2009 7:21 AM
> I think invariants should apply to subtypes, not just types.
> I think they are like constraints, and at least for scalars, can be
> checked in the same places.
I've not followed the recent discussion on invariants, but am not sure how
you deal with the usual invariant that is true most of the time but not
during atomic updates. Or a loop invariant that is true at the end of each
iteration but not during an iteration.
pre and post conditions are specific as to when they should evaluate to true,
but invariants cover a region (but not the whole program)
****************************************************************
From: Bob Duff
Sent: Thursday, February 26, 2009 7:40 AM
> I've not followed the recent discussion on invariants, but am not sure
> how you deal with the usual invariant that is true most of the time
> but not during atomic updates.
I'm not sure, either. That issue deserves some careful thought.
Perhaps scalars should be different from records?
>... Or a loop invariant that is
> true at the end of each iteration but not during an iteration.
Isn't the loop-invariant case just a "pragma Assert" written at some point
within the loop (e.g. at the end of each iteration)? I don't see any need for
a new feature for loop invariants.
The invariants I'm thinking of should apply to [sub]types. Maybe also to packages.
> pre and post conditions are specific as to when they should evaluate
> to true, but invariants cover a region (but not the whole program)
****************************************************************
From: Tucker Taft
Sent: Thursday, February 26, 2009 9:18 AM
> I think invariants should apply to subtypes, not just types.
> I think they are like constraints, and at least for scalars, can be
> checked in the same places.
We discussed this, and concluded that invariants and user-defined constraints
are both useful, but they are not the same thing. Invariants are generally
imposed on the implementation of an abstraction, and translate into
*postconditions* on all operations that return values to the "outside" world.
Constraints are often used as *preconditions* on values being passed *in* to
a subprogram, and generally are required to be satisfied at all points, whereas
invariants are often false in the middle of a primitive operation.
So we concluded, I believe, that invariants are associated with an abstraction,
and hence a type, or perhaps a package, while constraints define a subset of
the values of a type, and hence are appropriately associated with a subtype.
****************************************************************
From: Bob Duff
Sent: Thursday, February 26, 2009 7:57 AM
Question: In an invariant, does one refer to the "current instance" in the
usual way, by naming the [sub]type? As in:
type My_Int is range 0..1_000_000;
subtype My_Even_Int is My_Int with
Invariant => (My_Even_Int mod 2) = 0;
> I've not followed the recent discussion on invariants, but am not sure
> how you deal with the usual invariant that is true most of the time
> but not during atomic updates.
For scalars, one can use 'Base as always. E.g. if you have X: in out My_Int,
and you want to temporarily set it to a negative number, you do something like:
Temp : My_Int'Base := X;
Temp := Temp - 10; -- might be negative
Temp := abs Temp;
X := Temp; -- OK, Temp is now nonnegative
Similarly, My_Even_Int'Base would be a subtype that is NOT restricted to even
numbers.
Not sure how this can work for records.
By the way, I think the "in" operator should take invariants into account.
E.g.:
if Blah in My_Even_Int then ...
would be True iff Blah is an even number in the 0..1_000_000 range.
****************************************************************
From: Edmond Schonberg
Sent: Thursday, February 26, 2009 12:50 PM
> Question: In an invariant, does one refer to the "current instance"
> in the
> usual way, by naming the [sub]type? As in:
>
> type My_Int is range 0..1_000_000;
>
> subtype My_Even_Int is My_Int with
> Invariant => (My_Even_Int mod 2) = 0;
Invariants are intended for private types only. Otherwise the invariant
may have to be verified on assignment or any operation that would visibly
modify a value of the type outside of the defining package. This is
impractical and not particularly useful (we have constraints for this, and
invariants are NOT constraints). By limiting the invariant to a private
type, the check is limited to the visible primitive operations of the type
(what happens otherwise in the body stays in the body).
****************************************************************
From: Stephen Michell
Sent: Thursday, February 26, 2009 1:04 PM
In general, I like Tucker's proposal.
On the issue of invariance, Alan is completely correct. Invariance for,
say, the relationship between components or between state variables in a
class only allies when they are no threads executing subprograms that may
change that state.
You can make invariance work for every execution step, but in general that
is going to require auxillary variables and a lot of very hard work.
We need to develop syntax to express when invariance applies, or possibly
when it does not apply, such as loop invariants only apply at the exit
condition and state invariants only apply at the precondition and
postcondition points of every subprogram that can see the state.
As part of this effort, we need a syntax for auxillary variables, declaration,
assignment and formal relationships.
****************************************************************
From: Randy Brukardt
Sent: Thursday, February 26, 2009 1:49 PM
> I think invariants should apply to subtypes, not just types.
> I think they are like constraints, and at least for scalars, can be
> checked in the same places.
We talked about that at my insistence. We decided that invariants and
constraints are different things that solve different problems. (Which
is what I have been saying all along.) Invariants apply to all values of
a type, and can be inherited. Constraints apply to particular views (not
necessarily an object). Constraints are checked at the points that language
currently defines (subtype conversion); invariants are checked only when
crossing the boundary of the defining package.
I was tasked in writing up a proposal for user-defined constraints
(resurrecting my old proposal on that topic, but now using syntax and
legality rules).
If we can have only one of these, I think user-defined constraints are far
more useful. But I can see uses for both.
****************************************************************
From: Jean-Pierre Rosen
Sent: Friday, February 27, 2009 12:58 AM
> By limiting the invariant to
> a private type, the check is limited to the visible primitive
> operations of the type (what happens otherwise in the body stays in the body).
I understand limited to visible operations, but why primitives?
****************************************************************
From: Edmond Schonberg
Sent: Friday, February 27, 2009 2:57 PM
No reason, written in haste. Of course visible classwide operations are
included.
****************************************************************
From: Jean-Pierre Rosen
Sent: Saturday, February 28, 2009 5:11 AM
Actually, I was thinking of operations that are not primitive because they are
declared, f.e., in a subpackage.
****************************************************************
From: Yannick Moy
Sent: Monday, August 31, 2009 11:01 AM
I am forwarding here the beginning of a conversation with Ed Schonberg about
type invariants (AI05-0146), to be continued on this list.
Yannick Moy wrote:
> I have the feeling that the following rule stated for AI 05-0146 does
> not make it easy to check a type invariant:
>
>> > Invariants are only meaningful on private types, where there is a
>> > clear boundary (the enclosing package) that separates where the
>> > invariant applies (outside) and where it need not be satisfied (inside).
>
> The proposal only requires that (in) out parameters of primitive
> operations are checked, which does not seem sufficient to me. I also
> read the thread, and you seemed to agree with the proposal:
>
>> > Invariants are intended for private types only. Otherwise the
>> > invariant may have to be verified on assignment or any operation
>> > that would visibly modify a value of the type outside of the
>> > defining package. This is impractical and not particularly useful
>> > (we have constraints for this, and invariants are NOT constraints).
>> > By limiting the invariant to a private type, the check is limited
>> > to the visible primitive operations of the type (what happens otherwise in the body stays in the body).
>
> I do not see how this prevents violating the invariant of an object of
> that type different from the (in) out parameters, e.g., through a
> pointer. I have written a small example (attached) to explain my point.
> Do you agree there is a problem here, or did I miss something?
Ed Schonberg wrote:
> I agree that the proposal is not complete, and your neat example shows
> how to poke holes in it. I'm not sure that there is a formulation
> that is reasonably cheap to implement that would catch this example.
> Throughout the discussion there is of course a pragmatic thread: we
> cannot require implementations to do data-flow. Do you have a model
> for verification of invariants that would catch this case? Recall that
> this would have to be only for external calls, i.e. calls to Bad from
> outside of package A. I suspect that once you introduce indirection
> like this it becomes undecidable, and you don't want to put the check
> within the procedure body, because it may be an intended internal
> violation of the invariant.
Yannick Moy wrote:
>> I agree that the proposal is not complete, and your neat example
>> shows
>> > how to poke holes in it. I'm not sure that there is a formulation
>> > that is reasonably cheap to implement that would catch this example.
>
> I discussed it with Cyrille, and he also pointed to me that it is
> probably impractical to have an invariant that extends to "all objects
> of that type" at any given point in the program. In that case, an
> invariant is more like a shorthand for the equivalent set of pre- and
> postconditions, no more, and I think it should be emphasized in the
> wording of the problem section of the AI. In particular, the current
> wording is wrong, if we keep this notion of "never guaranteed true for
> all objects" invariant.
>
>> > Throughout the discussion there is of course a pragmatic thread: we
>> > cannot require implementations to do data-flow. Do you have a model
>> > for verification of invariants that would catch this case?
>
> Spec# ensures that the invariant
> obj.inv = "true" ==> obj.Inv()
> is always true, where "inv" is a hidden field of every object and "Inv"
> is the invariant of this particular object, by enforcing a detailed
> (and
> heavy) coding practice, in which an object must be "opened" explicitly
> before it is modified.
>
> JML does not ensure anything: invariants in JML are really just
> shorthands for pre- and postconditions.
>
> In our case, I think a very simple restriction would guarantee that
> the invariant is really valid for all objects of that type, outside of
> the part of the call-graph dominated by a procedure of package A
> (which may still include code outside of A): forbid modification of an
> object of that type that is not an (in) out parameter!
>
>> > Recall that this
>> > would have to be only for external calls, i.e. calls to Bad from
>> > outside of package A. I suspect that once you introduce
>> > indirection like this it becomes undecidable, and you don't want to
>> > put the check within the procedure body, because it may be an
>> > intended internal violation of the invariant.
>
> I agree that modification through an access type makes any static
> verification of the invariant undecidable. So either we forbid it, or
> we loosen the interpretation of 'invariant' (or we have 2 different
> kinds of invariants, kind-of weak and strong invariants?)
****************************************************************
From: Yannick Moy
Sent: Monday, August 31, 2009 1:51 PM
Attaching the example mentioned in the previous mail.
package A is
type T is private;
-- with Invariant => Ok(T);
function Ok (This : in T) return Boolean;
procedure Bad (This : in out T);
private
type T is record
J : Integer;
Next : access T;
end record;
end A;
package body A is
function Ok (This : in T) return Boolean is
begin
return This.J >= 0;
end Ok;
procedure Bad (This : in out T) is
begin
This.Next.J := -1;
end Bad;
end A;
****************************************************************
From: Steve Baird
Sent: Monday, August 31, 2009 3:32 PM
> I agree that modification through an access type makes any static
> verification of the invariant undecidable. So either we forbid it, or
> we loosen the interpretation of 'invariant' (or we have 2 different
> kinds of invariants, kind-of weak and strong invariants?)
And access types are just one way of running into this problem, right? A routine
which updates a global variable or a subcomponent of a parameter might result in
similar problems without involving access types.
Perhaps the name "Invariant" suggests something stronger than what this
mechanism implements, but this mechanism still seems like it might save a lot of
duplicated pre- and post-conditions. If we want to keep the mechanism but change
the name, someone will have to come up with a better name than Weak_Invariant or
I_Sure_Hope_This_Is_Usually_True .
****************************************************************
From: Bob Duff
Sent: Monday, August 31, 2009 5:21 PM
> In our case, I think a very simple restriction would guarantee that
> the invariant is really valid for all objects of that type, outside of
> the part of the call-graph dominated by a procedure of package A
> (which may still include code outside of A): forbid modification of an
> object of that type that is not an (in) out parameter!
Can you explain that a bit more? I'm not sure why it works.
> I agree that modification through an access type makes any static
> verification of the invariant undecidable. So either we forbid it, or
> we loosen the interpretation of 'invariant'...
In Eiffel, an invariant is just a short-hand for a bunch of pre- and
postconditions. Eiffel requires checking the invariant (at run time) on both
entry and exit of each method. The reason is basically the same as in your
example -- pointers. It's worse in Eiffel, because pointers are more
ubiquitous.
In an Ada context, if we follow the Eiffel ideas, we would check the invariant
for an 'in' parameter on entry to a procedure.
But that's uncomfortable. It is the responsibility (conceptually) of the
package itself to make sure the invariant is always true (for some definition of
"always" ;-)). But preconditions are the responsibility of the caller. How is
the caller supposed to ensure an invariant? It can't.
>... (or we have 2 different kinds
> of invariants, kind-of weak and strong invariants?)
I've thought about that a little. I wonder if it makes sense to let the
compiler decide which are weak and strong (as opposed to letting the programmer
label them)?
It sure would be nice if at least _some_ invariants are statically provable. It
seems hopeless to prove an invariant, unless you can somehow know that checking
the invariant on exit from a subprogram (for '[in] out' params and function
results) implies that the invariant _must_ be true on entry (for 'in [out]'
params). If you know that, you have some hope of doing an inductive proof.
Do we need 'globals' annotations, in the SPARK sense?
****************************************************************
From: Randy Brukardt
Sent: Monday, August 31, 2009 8:18 PM
> > In our case, I think a very simple restriction would guarantee that
> > the invariant is really valid for all objects of that type, outside
> > of the part of the call-graph dominated by a procedure of package A
> > (which may still include code outside of A): forbid modification of
> > an object of that type that is not an (in) out parameter!
>
> Can you explain that a bit more? I'm not sure why it works.
I don't think it does work, because the problem is modification of a logical
portion of the object that is not actually a part (in the technical sense) of
the object (that is, something that is accessed by a pointer rather than being a
(sub)component of the object).
OTOH, modifications of logical parts of "in" objects that have invariants via
pointers can be detected, and one could imagine having a warning about doing so
damaging the meaning of invariant. But it would be pretty nasty to make such
code illegal (especially as you can't tell for sure if pointer points at a
logical part of the current object, or at some other object).
...
> It sure would be nice if at least _some_ invariants are statically
> provable.
> It seems hopeless to prove an invariant, unless you can somehow know
> that checking the invariant on exit from a subprogram (for '[in] out'
> params and function results) implies that the invariant _must_ be true
> on entry (for 'in [out]' params). If you know that, you have some
> hope of doing an inductive proof.
>
> Do we need 'globals' annotations, in the SPARK sense?
Yes, absolutely. Without them, you can't do anything much statically with
preconditions/postconditions either, because the compiler cannot know whether
there are any side-effects in the predicate functions (there shouldn't be, but
if there are, it would be evil for a compiler to *introduces* erroneousness
because it removes/changes side-effects in preconditions. Adding preconditions
ought never make the program less safe!) The same is true for invariants.
Tucker and I had discussed this in the context of some previous discussion, and
we had gotten as far as trying to sketch out the form of such annotations. But
we didn't quite agree on the details, and we agreed to put it off until later.
(I believe this was just before the Brest meeting.) I suppose "later" is rapidly
approaching...
Note that I'd been trying to solve this problem with rules about purity, but
using globals annotations for that seems to work even better, being far more
flexible. They also (appear) easy to enforce, and since they're optional, there
shouldn't be any problem with enforcing them (if you can't write an enforcable
globals annotation, then don't write one at all).
****************************************************************
From: Robert C. Leif
Sent: Tuesday, September 1, 2009 9:28 AM
I have three questions:
1. Could some of the invariants be checked at compile time and not need to be
checked at run time?
2. Could the units of a numerical value be part of the invariants and be
checked as precondition and the units of returned values or out values be
checked as a post-condition?
3. Could item 2 be limited to compile time checking?
It should be noted that starting with Bill Whitaker some of us have been waiting
for an elegant, efficient solution in Ada to the units problem.
****************************************************************
From: Yannick Moy
Sent: Tuesday, September 1, 2009 1:47 AM
>> In our case, I think a very simple restriction would guarantee that
>> the invariant is really valid for all objects of that type, outside
>> of the part of the call-graph dominated by a procedure of package A
>> (which may still include code outside of A): forbid modification of
>> an object of that type that is not an (in) out parameter!
>
> Can you explain that a bit more? I'm not sure why it works.
There are 2 sides to this, as the comment from Randy Brukardt shows:
1) do not allow the invariant to mention anything beyond the value or the direct
fields in the private type;
2) only allow to violate the invariant of those objects which invariant will be
checked on subprogram exit, which are the [in] out parameters.
This is quite restrictive, as you cannot mention a value through an access type
in the invariant, even if it is through a field of the private type.
> In an Ada context, if we follow the Eiffel ideas, we would check the
> invariant for an 'in' parameter on entry to a procedure.
But we would not even be better off wrt this notion of strong invariants.
>> ... (or we have 2 different kinds
>> of invariants, kind-of weak and strong invariants?)
>
> I've thought about that a little. I wonder if it makes sense to let
> the compiler decide which are weak and strong (as opposed to letting
> the programmer label them)?
I guess that depends on what you allow in the invariant. In general, it would
not be feasible to decide whether an external call modifies an object by just
looking at the declarations. But if you stick to rule (1) above, where an
invariant only mentions value or direct fields of the private type, then only
the subprograms in the current package can modify the value of the invariant.
> It sure would be nice if at least _some_ invariants are statically provable.
> It seems hopeless to prove an invariant, unless you can somehow know
> that checking the invariant on exit from a subprogram (for '[in] out'
> params and function results) implies that the invariant _must_ be true
> on entry (for 'in [out]' params). If you know that, you have some
> hope of doing an inductive proof.
There are 2 parts in this verification:
- checking that every subprogram that could violate the strong invariant does
ensure it holds on exit. This is hard, usually needing some interaction of a
user with provers. Better left as dynamic checks in general.
- checking that outside of the parts of the call-graph dominated by a call which
could violate the strong invariant, the strong invariant holds. This should be
very easy, by restricting the kind of invariants as in rules (1) and (2)
above.
> Do we need 'globals' annotations, in the SPARK sense?
Not for strong invariants I think, but a common description of effects would be
great for any modular analysis of Ada, yes! Except we need more that SPARK, to
describe "any field Next reachable from this parameter" and other locations on
the heap.
****************************************************************
From: Yannick Moy
Sent: Tuesday, September 1, 2009 4:17 AM
> I don't think it does work, because the problem is modification of a
> logical part of the object that is not actually a part of the object
> (that is, something that is accessed by a pointer rather than being a
> (sub)component of the object).
You are right, I answered to this too when I answered to Bob. The key to strong
invariant is maintaining a kind of 'ownership' between an object and the parts
of state that are mentioned in its invariant.
> OTOH, modifications of logical parts of "in" objects that have
> invariants via pointers can be detected, and one could imagine having
> a warning about doing so damaging the meaning of invariant. But it
> would be pretty nasty to make such code illegal (especially as you
> can't tell for sure if pointer points at a logical part of the current object, or at some other object).
I am not sure if we want to go into such complexity. If the invariant is allowed
to talk about things that are pointed-to, then it is probably simpler to just
stick to weak invariants, that are only true when they were just checked.
> Tucker and I had discussed this in the context of some previous
> discussion, and we had gotten as far as trying to sketch out the form
> of such annotations. But we didn't quite agree on the details, and we
> agreed to put it off until later. (I believe this was just before the
> Brest meeting.) I suppose "later" is rapidly approaching...
Do you have a pointer to these discussions? I would be very interested in
reading your sketch of annotations.
> Note that I'd been trying to solve this problem with rules about
> purity, but using globals annotations for that seems to work even
> better, being far more flexible. They also (appear) easy to enforce,
> and since they're optional, there shouldn't be any problem with
> enforcing them (if you can't write an enforcable globals annotation, then
> don't write one at all).
Great! I'd be happy to be part of that discussion too.
****************************************************************
From: Randy Brukardt
Sent: Tuesday, September 1, 2009 1:36 PM
> It should be noted that starting with Bill Whitaker some of us have
> been waiting for an elegant, efficient solution in Ada to the units
> problem.
Don't hold your breath. Lots of very smart people (including Tucker) have tried
to address the units problem, and no "elegant, efficient" solution (that is
correct as well) has been found. Solutions that work either require runtime
checks (meaning not so efficient) or generating an extremely complex set of type
definitions (efficient, but not elegant). The best solution I've seen uses a
program to generate the nest of type and operator definitions needed for an
efficient solution. Part of the problem is that the interelationships between
units are not fixed; there are lots of different combinations. So it isn't
practical to include those relationships in a programming language.
****************************************************************
From: Randy Brukardt
Sent: Tuesday, September 1, 2009 1:42 PM
> > Tucker and I had discussed this in the context of some previous
> > discussion, and we had gotten as far as trying to sketch out the
> > form of such annotations. But we didn't quite agree on the details,
> > and we agreed to put it off until later. (I believe this was just
> > before the Brest meeting.) I suppose "later" is rapidly approaching...
>
> Do you have a pointer to these discussions? I would be very interested
> in reading your sketch of annotations.
It was just in private e-mail; it never got far enough along for public
consumption. I was stuck on finding a reasonable form for listing specific
objects accessed. It seems to be a some sort of list, but the resolution rules
for that list are hard to explain (any object plus keywords null and private?).
> > Note that I'd been trying to solve this problem with rules about
> > purity, but using globals annotations for that seems to work even
> > better, being far more flexible. They also (appear) easy to enforce,
> > and since they're optional, there shouldn't be any problem with
> > enforcing them (if you can't write an enforcable globals
> annotation, then don't write one at all).
>
> Great! I'd be happy to be part of that discussion too.
I'll try to make sure something is proposed well before the November meeting (it
has to be, or it can't be included in Amendment 2). Once we have an outline, we
can then throw brickbats, I mean discuss the details.
****************************************************************
Questions? Ask the ACAA Technical Agent