Split Capabilities: Making Capabilities Scale

[Karp, Alan]

> -----Original Message-----
> From: Mark S. Miller [mailto:markm@caplet.com]
> Sent: Monday, July 31, 2000 11:51 AM
> To: Karp, Alan
> Cc: 'Jonathan S. Shapiro'; 'Ralph Hartley'; e-lang@eros-os.org
> Subject: RE: Split Capabilities: Making Capabilities Scale
> 
> 
> At 11:29 AM 7/31/00 , Karp, Alan wrote:
> >We're allowed to use symbolic notation in our state 
> transition diagrams,
> >aren't we?  Pardon the poor notation.
> >
> >                 construct(int x): x<=0; exception; X = x
> >                                         
> >                 decrement() X:=X-1
> >
> >                         X==0: BlastOff(); 
> destruct()(object, not rocket)
> 
> This is no longer a state transition diagram, as it no longer 
> expresses a 
> *finite* state machine.  We can certainly allow ourselves 
> whatever notation 
> we want, but different choices will have different formal 
> properties.  Do 
> you intend the above notation to have different properties 
> than a program in 
> an OO programming language?  If so, what?  If not, how is 
> this different 
> than using an implementation as an executable specification?  
> Executable 
> specifications are fine things.  I'm just trying to 
> understand what you're 
> saying.

I knew the notation would get me in trouble.  The methods (e.g., decrement)
represent arcs; the statements (X:=X-1) the new state in terms of the old
state.  A getX() method would have an arc taking X back into itself (X:=X).
The if statement is part of the state transition.  It says there is no
externally visible state with a value of 0; the object destroys itself.  As
a side effect, blast off occurs.  I don't really know the proper notation
for this.

I'm not real strong on formal methods, but I've used state transition
diagrams to good effect to describe the implications of various invocations.
It was my hope that they could be used to describe the contract (If you do
A, then B will happen.) of the object behind the facet.

> 
> In any case, any formal notation for which the above is an 
> example is much 
> more powerful than a finite state machine, and probably has 
> the normal 
> Turing/Godel undecidability limits.  After all, it's got 
> integer (or at 
> least Peano) arithmetic!

You know more about this stuff than I do.  I understand that undecidable
things exist, but I didn't think that implied that nothing is decidable.  I
believe you can prove that a countdown object that is initialized to 10 and
has only a decrement by 1 operation will reach 0 in a finite number of
decrements.  If you also have an increment operator, you can make no such
statement.  You may still be able to prove it reaches 0, but you must look
at how it is used.  (Two steps down and one up, for example.)

> 
> 
>          Cheers,
>          --MarkM
> 

_________________________
Alan Karp
Decision Technology Department
Hewlett-Packard Laboratories MS 1U-2
1501 Page Mill Road
Palo Alto, CA 94304
(650) 857-3967, fax (650) 857-6278