Loading...
Please wait, while we are loading the content...
Separating Algorithm and Implementation in the Refinement of Parallel Program Specifications
| Content Provider | Semantic Scholar |
|---|---|
| Author | Roegel, Denis |
| Copyright Year | 1996 |
| Abstract | Correct concurrent programs can be obtained through the re nement of abstract speci cations. 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 + speci cation, 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 de ned 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 in nite 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 |
| DOI | 10.14236/ewic/rw1996.12 |
| Alternate Webpage(s) | https://www.scienceopen.com/document_file/586d2d67-9615-40d9-b2ac-575de32e26fb/ScienceOpen/001_Roegel.pdf |
| Alternate Webpage(s) | https://doi.org/10.14236/ewic%2Frw1996.12 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
