Object-Oriented Specification by Typed Gurevich Machines

An approach to the object-oriented specification by typed Gurevich machines is proposed in the paper. The approach is based on considering an object update as a transition from one algebra of a given signature to another of the same signature. Each object possesses a state and a unique identifier; the state of a mutable object can be updated, the state of a constant object cannot be updated. An algebra provides two sets of unique identifiers for each object type: a set of mutable object identifiers and a set of constant object identifiers. An object type signature introduces the observers of the corresponding set of objects serving to inspect object states and mutators serving to initialize and update observers of mutable objects. Transition rules of a typed Curevich machine are proposed as a means of object specification. The specification methodology is quite straightforward: an object initialization or modification by means of a mutator is expressed in terms of updates of the object’s observers.