Abstract | ||
---|---|---|
This paper explores a compositional approach to program specification, development and proof. We apply a theory of composition to a problem in distributed computing with the goal of understanding the strengths and weaknesses of this compositional approach. First, we describe the theory briefly. Then we give a specification of a desired system. Next, we propose a design of the desired system as a composition of components and prove its correctness. Finally, we show how the proof can be reused for a slightly different compositional structure by using the concept of observation. |
Year | DOI | Venue |
---|---|---|
2002 | 10.1023/A:1012952311559 | Formal Methods in System Design |
Keywords | Field | DocType |
composition,formal specification,program verification,temporal logic,UNITY | Programming language,Computer science,Correctness,Theoretical computer science,Formal specification,Program derivation,Temporal logic,Strengths and weaknesses,Program specification | Journal |
Volume | Issue | ISSN |
20 | 1 | 1572-8102 |
Citations | PageRank | References |
12 | 0.88 | 7 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
K. Mani Chandy | 1 | 6606 | 1842.49 |
Michel Charpentier | 2 | 12 | 0.88 |