A semantic framework for formalizing _(distributed), concurrent _(object-oriented) system, so that verifying their behavior is much-simplified. See the _(home page| http://www-cse.ucsd.edu/users/goguen/projs/halg.html) or _(CafeOBJ), which implements the semantics.
