A Caltech Library Service

An Experiment in Program Composition and Proof

Chandy, K. Mani and Charpentier, Michel (2002) An Experiment in Program Composition and Proof. Formal Methods in System Design, 20 (1). pp. 7-21. ISSN 0925-9856. doi:10.1023/a:1012952311559.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


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.

Item Type:Article
Related URLs:
URLURL TypeDescription ReadCube access
Additional Information:© 2002 Kluwer Academic Publishers. This work is supported by a grant from the Air Force Office of Scientific Research.
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)UNSPECIFIED
Subject Keywords:composition; formal specification; program verification; temporal logic; UNITY
Issue or Number:1
Record Number:CaltechAUTHORS:20191112-111040108
Persistent URL:
Official Citation:Chandy, K.M. & Charpentier, M. Formal Methods in System Design (2002) 20: 7.
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:99808
Deposited By: Tony Diaz
Deposited On:12 Nov 2019 22:53
Last Modified:16 Nov 2021 17:49

Repository Staff Only: item control page