Formal Properties of the Eiffel// Model

Featuring a small set of concepts (e.g. systematic asynchronous communications, polymorphism between passive and active objects, wait-by-necessity) the Eiffel// model allows for the derivation of parallel systems from sequential ones. Based on a formal semantics of that model, this article expresses and formally proves language properties such as the absence of shared objects, the sequentiality of subsystems. Moreover, equivalence of programs, sequential vs. parallel, can also be demonstrated in some cases. This work is a first step towards automatic (or semiautomatic) parallelization of object-oriented programs