Typed Gurevich machines revisited

An approach to combining type-structured algebraic specifications with Gurevich Machines (evolving algebras) is proposed. A type-structured algebraic specification, in its simplest form, consists of data type specifications and independent function (detached operation) specifications. Concrete and generic specification components (data types and functions) are distinguished in a more developed case. A type-structured algebraic specification is augmented by a number of transition rules of a conventional Gurevich Machine indicating in which way an algebra of a given signature evolves to another algebra of the same signature. A function update is a primitive algebra transformation. Two classes of functions are distinguished, static functions which do not change when an algebra evolves, and dynamic functions which do change when an algebra evolves. Data type operations are static. The semantics of data types and static functions is given by axioms, the semantics of dynamic functions is given by transition rules.