The main objective is to define a formal semantics of Eiffel// in order to be able to achieve formal transformations (parallelization); the ambition is not to develop new results in the domain of the semantics of parallelism itself. It will be required to define a formal model of execution for both Eiffel and Eiffel// which permits to prove the equivalence of two programs after a transformation.
A specific formal model will have to be defined
but it will rely as much as possible on existing models of
concurrent computations and equivalence relations
(CSP, CCS, Meije, ACP, -calculus, actors)
[3][76][75][59][12][10][73][61]
We are currently studying what are the models and representations
which are better adapted to the kind of proofs
we need to achieve. Then, we probably will need to develop
specific adaptations, restrictions, or extensions.