Refinement in a Concurrent, Object-Based Language

P. Blauth Menezes
UFRGS

A. Sernadas
Universidade Técnica de Lisboa, Portugal

J. Félix Costa
Universidade de Lisboa, Portugal

Nonsequential automata constitute a categorial semantic domain based on labeled transition system with full concurrency, where restriction and relabeling are functorial and a class of morphisms stands for refinement. It is, for our knowledge, the first model for concurrency which satisfies the diagonal compositionality requirement, i.e., refinements compose (vertical) and distribute over combinators (horizontal). To experiment with the proposed semantic domain, a semantics for a concurrent, object-based language is given. It is a simplified and revised version of the object-oriented specification language GNOME, introducing some special features inspired by the semantic domain such as refinement. The diagonal compositionality is an essential property to give semantics in this context.
.