Split Capabilities: Making Capabilities Scale

Ralph Hartley hartley@AIC.NRL.Navy.Mil
Mon, 31 Jul 2000 14:16:40 -0400


> > > and would not let von Braun use the object to count down to launch.
> > > He could if the definition was "The do method decreases the
> > > value of the
> > > count by 1.  Launch occurs when the count reaches 0.".

If I were on Braun I would never accept that as a contract for a
countdown object. He needs at least :

The count is a non-negative integer that is initially ten.
When on Braun uses his decrement message the count decreases by
  at most one.
The count will never decrease at any other time.
If the count is less than ten and the count has
  decreased in the last second the count will
  not decrease.
Whenever the count decreases to a value less than ten
  the new value is broadcast on the PA system (so that
  everyone can hear).
Launch may occur when the count reaches 0.

This contract does not describe all of the countdown object's state
transitions. It does not mention the possibility that the count might
increase at all. One cannot do complete reasoning about it. But one
can make some inferences:

No one but on Braun can trigger a launch.
No one will ever be surprised by a launch, everyone will
  have at least ten seconds notice.

Suppose on Braun's programmer has a copy of the source code for the
countdown object and he notices that the count can never increase. Can
he use this fact? No, it would be an error to do so. Someone might
notice after van Braun was written that the range safety officer needs
to be able to cancel a launch, and that many other people need to be
able to delay it. It is legal to rewrite the counter object so that
the countdown can be stopped or incremented, since such an
implementation is not forbidden by the contract.

Nor should the fact that in all the test runs launch occurs after
exactly ten calls to decrement cause on Braun to be surprised on the
day of the launch when launch happens after 127 decrements. Nor should
anyone be surprised when launch occurs 15 seconds after the PA system
announces "count = 30" (the count might not have really been 30 or on
Braun may have decremented 20 times in five seconds then once per
second for 10 seconds). But if launch occurs without the numbers 1-9
being announced then the countdown object is broken.

> That's just great.  Now von Braun doesn't know what might happen.  If the
> count can start negative, he can't use it for his launches.  How many other
> possibilities must he worry about?  Can it decrement by 7 at random?  Can
> the value turn into a floating point number?  A string?   Why not?  Nobody
> said it couldn't happen.  I don't think I'd like writing programs under such
> conditions.

You (I think it was you, I might have lost track) wrote the contract
not me. To prove a system correct (which is what I assume you would
like to do by "reasoning about objects", you must prove that each
object (or facet) fulfills its contract assuming all objects or facets
it uses fulfill theirs, and that the system meets its specification if
all its objects fulfill their contracts.

> > > Of course, this is all off the point, which is to answer
> > the following
> > > question.  If object is state plus (externally visible)
> > behavior, can I
> > > reason about a facet as an object?  My contention is that I
> > can't because
> > > I'm missing information about the legal state transitions.
> >
> > You can still reason about an object who's contract does not
> > completely determine its visible behavior. The results of your
> > reasoning will just be weaker, that's all. People reason about things
> > without complete descriptions all the time (literally).
> 
> Yes, I can reason about the object, but incompletely.  It is exactly the
> incompleteness of the view of the object presented by a facet that leads me
> to believe that I can't reason about the facet as an object.  It is this
> imprecision that leads to software failures (people failures, too).  Failing
> to specify my units may cause my spacecraft to miss Mars.  Relying on a
> poorly worded contract may lead to a law suit.

It is far more important that your reasoning be sound than that it be
complete. In fact, it is generally impossible for reasoning to be both
(Godel and all that). It is not imprecision that causes errors, it is
unjustified assumptions. Assuming that a counter can never increase,
just because you have not been told that it can, or because it never
has, or because examination of the internal code of an object (unless
the objects contract specifies that it will always be implemented by
that code) shows that it never does, is an example.

A facet is simply an object who's implementation is provided by
another object. Its contract will in general be different from that of
the underlying object. In the case of a thinning, its contract will
generally be weaker, in the sense that the underlying object can
always substitute for the facet, but not the other way around.

Note that under this definition, an object and a thinning of the
object may implement exactly the same methods using exactly the same
code, and still be different if they promise different contracts. For
instance a countdown object could be correctly implemented as a facet
of a non-increasing countdown object.

Ralph Hartley