Concurrent state transformations on abstract data types

Abstract

The introduction of a notion of states into algebraic specifications yields the possibility to specify dynamic and communicating systems, and to compare formally algebraic and dynamic specifications. In the approach presented here states are modelled as partial algebras that extend a fixed partial algebra considered as static data type. Transitions are specified by rules that express the replacement of properties when passing from one state to another. In this framework parallel and concurrent composition of transitions and their representation are investigated. Furthermore a restriction of the general approach to a specification framework for environment transformations is presented. It allows the specification of dynamic systems based on dynamic entities like pointers, and has the same structural properties as the algebraic specification logic.