Title
An Experiment in Program Composition and Proof
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 Chandy166061842.49
Michel Charpentier2120.88