Re: [boost] Re: "invariants" class; Version 1.00

From: Tanton Gibbs (thgibbs_at_[hidden])
Date: 2004-01-08 07:09:22

> > I wrote a framework and a paper on Temporal Invariants.  These
invariants
> > exist or are freed over time.  You might get some interesting ideas from
the
> > paper; a link is attached.
> >
> > http://www.cs.clemson.edu/~malloy/papers/csmr03/temporal/paper.pdf
>
> Very interesting. I've many times written invariants only to remove them
> later on finding that they didn't always apply.

Definitely, we have run into cases with circular dependencies where
invariants
don't exist at first, then exist forever after a certain point (that would
be an EventuallyThenAlways, which is not mentioned in the paper).  In fact,
any object that cannot fully initialize on creation will have some form of
this problem.

> I'm only half way through the paper, so perhaps my questions are
> premature. It would seem to me that two of the keywords depend on the
> other two, namely,
>
> always  ==  ! never

This is true, never was provided for readability/convienence.

> And having 'already' seems to make 'eventually' unnecessary.

That is true as well, though I tend to see them used for very different
purposes.  Eventually is more of a resource management tool.  Eventually
this pointer is freed, eventually this file is closed, eventually my
circular dependency will be resolved and I will have created something that
has a pointer back to me.  Already can be used for these type things as
well, but saying it as eventually makes more sense to me :-)

>I have only
> a boolean (char actually) in my invariants class, and I'm planning to
> get rid of it, as having state in the invariants class is an invitation
> for for using invariant checks on invariant base itself. So I wish not
> to have to store whether 'eventually' has indeed ever come true. And
> this may not be justified anyhow:

Yep, who watches the watchers.  You definitely have to weigh the gain vs the
loss in provable correctness.

> Suppose I have a class which at some point allocates a container. Until
> such container is allocated, some of the public functions may not apply.
> Now, all I need to debug un-timely calls to such functions are
> preconditions in those functions to the effect that the container exists
> 'already'. Admittedly, my use of the term "precondition" is misleading,
> since preconditions are the business of clients and must be expressed in
> terms of conditions visible to the client, as opposed to private vars.

In this case, what is the difference between saying the container exists
already and the container exists?  The difference between an already
invariant and a plain invariant is that the already invariant shuts off as
soon as it is shown true.  A plain invariant that doesn't shut off is
equivalent to AlreadyThenAlways (not shown in paper).  However, that
requires state to say whether or not it has been executed, so there is
really no reason for you to move away from regular invariants.

As for state in the invariant class, I can't say whether it is good or not.
I believe that it makes for more expressive invariants, but how often are
those needed?  I do believe one of the important points of the paper is to
use policies and aspects to weave invariants into the program automatically
instead of requiring programmer intervention (though the paper uses a manual
weaving process, automatic ones do exist).  As for all things, your mileage
may vary.

Tanton