Abstract state

I am struggling with the semantics and implementation of abstract state in my language dodo and I am looking for relevant papers or prior art.

These are the desired properties of abstract state I am after:

- A type can have different sets of attributes and methods depending on the abstract state of the object
- State transition can be ruled by an expression based on attributes of the object
- If the type is composed with mixin Tagged, then abstract state is stored in the tag
- A tagged type can define transition functions to go from one specific state to the other
- The abstract state cannot be set by other means than previously listed

The first property means that state transition basically changes the type of the object. I think of unions in C, or case classes in functional languages. The compiler needs to check the abstract state of the object to see if an operation on it is valid.

The second property defines a way to transition to a new state. In dodo, rules are enforced during validation of changes. Validation can be explicit (mutable object) or implicit.

The third property allows abstract state to be encoded in a variable. For polymorphic types, the type attribute and the abstract state tag are the same. The type of an object establishes its abstract state.

The last two properties ensure that state transitions occur in a controlled fashion. A transition function can either return an object in the new state (notably for immutable objects) or mutate the object, allowing it to assume the form required for the new state.

I am having trouble with the notion of an object changing its set of attributes and operations in the middle of a method, I don't know what would be a reasonable solution.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Looks like it...

That leads me to:


It looks like what I am looking for, thanks.

Behavioral Types

For objects that may change their interface after a method invocation, I suggest that you have a look at behavioral types, for instance the work of Vasconcelos and Ravara, see e.g. Behavioural types for a calculus of concurrent objects. Euro-Par'97 Parallel Processing, 1997

You have a very large body of works in this domain, see also the actor calculus of Colaço, Pantel and Sallé (http://www.irit.fr/-Publications-?code=239&nom=Pantel%20Marc), work by Elie Najm (http://perso.telecom-paristech.fr/~najm/) and, in a similar but more recent vein, work on sessions types.