Stepwise refinement and concurrency: The finite-state case (Q2640349)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Stepwise refinement and concurrency: The finite-state case |
scientific article |
Statements
Stepwise refinement and concurrency: The finite-state case (English)
0 references
1990
0 references
A method for the design and verification of finite-state concurrent programs is proposed that is a hybrid of a stepwise refinement and a fixpoint-based method, thus retaining the advantages of both, viz. efficiency plus clarity, and completeness, respectively. The method is illustrated by several examples, and special attention is paid to the case of sequential refinement which is used most frequently in practice.
0 references
stepwise refinement
0 references
concurrency
0 references
Hoare logic
0 references
fixed points
0 references
strongest postconditions
0 references
verification
0 references
