Specifying almost-real concurrent object-oriented programs

Parallel programming is difficult. The need for correct and efficient parallel programs is important and one way to meet this requirement is to work on the refinement chain. Beginning with a specification written in TLA⁺ (for instance), we can transform it-or refine it-into finer grained specifications. At some step, enough structure will have appeared so that we can bridge a gap to fill this structure. We introduce a more concrete version of TLA⁺ , CTLA, where structuring concerns are to be expressed, but where distributing, mapping or implementation problems are avoided. Indeed, we firmly believe that it is a mistake to go immediately from TLA⁺ to a real language like CC++, since the ditch is still too wide. A numerical example supports our claim