Separating Algorithm and Implementation in the Refinement of Parallel Program Specifications

Correct concurrent programs can be obtained through the refinement of abstract specifications. In this paper, we explore a methodology, which we call task separation , in which we split the development of a program in two phases: a first stage where an algorithm is introduced from a TLA + specification, but where the data structures remain unconstrained; a second stage where the other aspects of the program are dealt with. The intermediate state can be represented in an object-oriented way, emphasizing its relationship with languages like C++. This notation, cTLA (concrete TLA) is defined semantically in TLA + and aims to provide a fair representation of an algorithm, compared to TLA + ’s at rendering. cTLA’s types and values are the values in TLA+. cTLA’s class instances are processes, and there are virtually an infinite number of processes, which can be activated. A numerical example, the block decomposition algorithm in the matrix multiplication, supports our views.