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.
Author and article information
Campus scientifique — BP 239
54506 Vandœuvre-lès-Nancy cedex, France