States as Specifications
Paulo Borba
UFPE
We present a general approach for formally modelling
states of object-oriented programs using OBJ
specifications and associated order-sorted theory presentations.
This formal model can then be used to define the structural
operational semantics of object-oriented languages.
Our approach has the advantage of using the power of the theory
of abstract data types for defining operations on states.
As states are represented by an abstract structure, the
operational semantics can be defined in a simpler way,
facilitating reasoning about programs and derivation of
implementations.
.