Specifying almost-real concurrent object-oriented programs
Denis Roegel · 2002
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/sup +/ (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/sup +/, 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/sup +/ to a real language like CC++, since the ditch is still too wide. A numerical example supports our claim.