Name
Abstract | ||
|---|---|---|
Typically, program design involves constructing a program, P, that implements a given specification, S; that is, the set P'' of executions of P is a subset of the set S'' of executions satisfying S. In many cases, we seek a P that not only implements S but for which P'' = S''. Then, every execution satisfying the specification is a possible execution of the program; we call P maximal for the specification S. We argue in this paper that traditional specifications of concurrent programs are incomplete without some maximality requirement because they can often be implemented in a sequential fashion. Additionally, a maximal solution can be refined to a variety of programs each appropriate for execution on a different computing platform. In this paper, we suggest a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for many non-trivial examples. The method may also serve as a guide in constructing maximal programs. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/s001650070031 | Formal Asp. Comput. |
Keywords | Field | DocType |
Keywords: Concurrent program design,Safety,Progress,Maximal solution | Programming language,Concurrency,Computer science,Theoretical computer science,Linear temporal logic,Program Design Language,Mathematical proof,Branching (version control) | Journal |
Volume | Issue | ISSN |
12 | 2 | 0934-5043 |
Citations | PageRank | References |
2 | 0.45 | 6 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rajeev Joshi | 1 | 2 | 0.45 |
| Jayadev Misra | 2 | 3147 | 771.78 |