Loading...
Please wait, while we are loading the content...
Separating Algorithm and Implementation in the Re nement ofParallel Program
| Content Provider | Semantic Scholar |
|---|---|
| Author | Roegel, Denis |
| Copyright Year | 1996 |
| Abstract | Correct concurrent programs can be obtained through the reenement of abstract speciications. 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 rst stage where an algorithm is introduced from a TLA + speciication, 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 deened 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 innnite number of processes, which can be activated. A numerical example, the block decomposition algorithm in the matrix multiplication, supports our views. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.loria.fr/~roegel/Articles/facs-revised.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
