Prev Up
Go backward to Mizar Verification of Generic Algebraic Algorithms
Christoph Schwarzweller

Go up to Specification and Verification

Language Independent Container Specification
Alexandre Zamulin

The purpose of this talk is to propose an iterator and container specification mechanism which makes the specification independent of a particular Programming Language and makes the specification formal. The following options have been considered:

The chosen technique, called Object-Oriented Gurevich Machine, combines advantages of both approaches mentioned above. It permits conventionally specifying a needed set of data types and specifying by transition rules a needed set of object types. An object is an entity possessing a unique identifier and a state. It is characterized by a number of attributes defining its state and a number of methods for observing (observers) and changing (mutators) the state. An object type defines a set of states of a particular object.

An iterator is represented as an object of the corresponding iterator type with an address as the object's identifier. Iterator types are combined in iterator categories each having a definite set of iterator operation. A container is represented as an object of the corresponding container type possessing a number of attributes, observers, and mutators. Observers are specified in terms of attribute values. Mutators are specified in terms of transition rules updating attribute values.


Prev Up