Specifications

[Tril]

On 1 May 1999, Laurent Martelli wrote:

> 	"If the object disappears then your unique ID is
> 	useless. And, if you allow anyone to access an object
> 	if they know its ID, your system won't be very secure"
> 
> You say that the 1st issue can be tackled with a "two-way reference"
> so that references can be invalidated when the object is
> destroyed. Well why not. But what does it mean "to invalidate"
> references to an object ? We could very well do a runtime checking and
> see if the object referenced exists when we want to use it. And what
> about garbage collection ? 

The problem with checking if it exists, is that if it doesn't exist, some
other object may have taken its ID. (Then you may mistakenly think it
exists because the ID is in use) Therefore, we can't allow an object to be
deleted until all references to it are gone.  By invalidation, I meant
that the reference is actually deleted.  (Taken out of use, and queued for
deletion, marked for GC, whatever)  

I'm not a GC person, but I guess you could have the reference marked for
deletion, then the ID would be still in use until actual GC took place.  
Maybe a new object could get the ID while it's still waiting to be erased,
and the new object would be created at the same time as the other one is
deleted, making some delayed creation available?

> You solve the security problem by saying that the client will not be
> allowed to read the reference. By what can you do with it then ? 

It can use the reference to do any legal operation on the object.  It just
can't find the ID for the object.  

> I think that the security issue is one aspect of system, and it
> shouldn't interfere with the main functional aspect. Deciding who is
> allowed to use an object should be independent of what the object can
> do (it's functional aspect). This leads to a better reusability since
> you can reuse the functional aspect without being forced to reuse a
> security aspect that does not fit you needs. 

Each aspect, including security, is separated out in a separate orthogonal
type.  What you say is true, and is the intended design.

>         o Functions and Types
> 
> I agree that one argument is all you need. But I think that specifying
> a function only by its input and output type is a poor
> specification. In fact, I think of typing as a special case of
> pre/post conditions. If you allow any function to be used in the
> pre/post conditions, they can be arbitrarily complex, and you can
> fully specify what the function does (you don't need an implementation
> since it is contained in the post condition). Let's take an example :
> 
> if you have a function `F' which takes an integer and returns an
> integer, you don't know what it does. But if you say that the
> pre-condition is that the argument is an integer, and that the
> post-condition is that the result is such that `result = argument + 1'
> you have a _full_ specification of F, and there's no need to implement
> it. 

I completely agree with this method.  But I don't distinguish between
typing and pre/post conditions.  They're the same, therefore the full
specification of F is that it maps from the "integer" type to the 
"incremented integer" type.  Types are formed by conditions as you said,
and I do allow any function to be used as the condition.

If we do this universally, functions are simply links between two types.
All the information is in the type, and functions can be automatically
generated.  You won't have to explicitly USE a function, much less give it
a name "F".  Just select two types, and draw an "arrow" <grin> between
them.  The system does the rest. 

(Heavy use of this method would mean a LOT of types.  So in any program,
you will probably define a lot of types on the fly while the program is
running, instead of having a static group of predefined types.)

>         o Subtypes and Supertypes
> 
> Sets and subsets are one way to see things. But I believe that a
> behavioral understanding of the subject can also be very
> useful. Knowing that an object is part of a set of objects does not
> tell much about it. What you usually want to know is what you can do
> woth it, ie how it behaves. Have you read Liskov's papers about
> behaviour and inheritance ? (I don"t have pointer, and my ISP is down,
> sorry :-( ) It seems to me that the behavioral definition of types and
> subtypes is the only one which makes sense. 

You posted it before, I found in the archives:
  http://www.cs.cmu.edu/afs/cs/project/venari/www/subtype-toplas.html

Knowing an object is part of a set (defined by a condition being true)
DOES tell a lot about it because the set is directly used as the domain of
functions.  You can determine all the functions that use a type (because
the way they "use" the type is by linking to it, and these are one example
of two way links), and then you DO know what the object can do.  This is
basically the reason for types.  How is my notion different from
behavioral?  (I haven't read the paper, I will soon and post a commentary)

>         o Generic Functions
> 
> Since this paragraph is based on your definition of types and I don't
> agree with it, I don't agree with that one too :-) Especially when you
> say that a generic function "is a function with no definition of its
> own, but delegates to other functions". In fact this what all
> functions do. But the dispatching algorithm vary. If you think about
> it, all functions end up calling other functions (or themselves). 

Yes, all functions delegate, and that's just another reason why generic
functions aren't much different from regular functions.  But I mean a
generic function to be specifically one which dispatches on
the type of its argument, and it PASSES that same argument to the
sub-function chosen.  The sub-functions each have a precondition which is
a subtype of the precondition for the generic function, and link to the
generic function (to specify that they will be a method for that function,
we use linking instead of the traditional technique of making the
functions have the same name).

>         o Partial Evaluation
> 
> As I understand it, it's an optimisation technique. It may be
> interesting, but I do not want to talk about that now.
> 
> Laurent
> 

Thanks for your comments, they will be helpful in revising the
specification.

David Manifold <dem@tunes.org>
This message is placed in the public domain.