Re: Seeking for papers about tagged types vs access to subprograms

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 13-05-13 10:22 , Dmitry A. Kazakov wrote:
> On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:
> 
>> The point of the example was to illustrate typestate analysis. For this
>> example, with only Open - (Read/Write)* - Close, your approach collapses
>> the example into a trivial one, where adherence to the operation
>> protocol is ensured by the necessity to declare a File_Info object
>> before it can be used. So it would no longer be a useful example.
> 
> It is still a useful example of a good software component design.

Hm. In this thread, I think this example is interesting only if it can
show us alternatives to typestate analysis, giving the same verification
power by other means. I don't think this Open-in-declaration approach
(essentially removing the Open and Close operations from the problem)
applies in the general case, so I don't find it interesting in this thread.

>> Your approach works in some cases, but it is problematic if you cannot
>> initialize the object to an "active" state in its declaration, for
>> example because the "activation" is conditional in some way, or must be
>> delayed.
> 
> This is rather a language problem. Most of such cases can be attributed to
> the lack or insufficient constructors. The notorious Ada's problem with
> task components is due to the lack of class-wide constructors, when
> Initialize tries to sit on two chairs struggling to be both a specific and
> a class-wide initialization.

The initialization step, which is just the first state transition of an
object, is only a small part of the problem for typestate analysis.

>> The "activation" must then be done in a statement, and the
>> declaration leaves the object in some inactive initial state.
> 
> That is not a problem so long this state is not exposed. The idea is that
> when you have an object which may transit from state to state (e.g. a
> connection object, when the connection can be lost), you should not expose
> this state.

Even if the state is hidden from the clients, it is present internally,
and must be considered in any analysis of correctness.

> You better make the object to maintain the state (e.g. by
> making the connection restored by the object automatically) and leave its
> interface free of the state (e.g. an operation on unconnected object would
> block or else raise Busy_Error etc).

Here "unconnected object" is analogous to "closed file". The state
exists, even if hidden from clients. In fact, from the point of view of
typestate analysis, the state is or should be visible, since it affects
the availability or success of operations on the object.

The goal of typestate analysis, even of client code, is to show if
operations can be illegally applied and thus fail, for example by
raising Busy_Error. For this, the analysis must include the
"unconnected" state.

>> Another limitation in your approach is that the opening and closing of
>> different files must be strictly nested: if you declare and open file A,
>> then declare and open file B, file B must be closed before file A is
>> closed (as long as it all happens in the same task). Such forced
>> constraints between the states of different object is often not wanted.
> 
> You can have a container, e.g. a bag, to handle this.

This introduces a new object -- the container -- with its own, perhaps
more complex state: whether or not it contains the object (e.g. a
File_Object) that is our real interest. Not a good idea, I think.

> Jeffrey's model translates this into the problem of object's scope
> (lifetime), which saves time and mental efforts.

Only in this special case, the "file" example, where the state structure
is so simple that after hiding the first state transition (Open) into
the construction of the object, and the last state transition (Close)
into the destruction, there is only one state left (Is_Open), which
makes typestate analysis trivial.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .