CaltechAUTHORS
  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. https://resolver.caltech.edu/CaltechAUTHORS:20191112-111040108

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

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20191112-111040108

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.


Item Type:Article
Related URLs:
URLURL TypeDescription
https://doi.org/10.1023/a:1012952311559DOIArticle
https://rdcu.be/bWGexPublisherFree ReadCube access
Additional Information:© 2002 Kluwer Academic Publishers. This work is supported by a grant from the Air Force Office of Scientific Research.
Funders:
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
DOI:10.1023/a:1012952311559
Record Number:CaltechAUTHORS:20191112-111040108
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20191112-111040108
Official Citation:Chandy, K.M. & Charpentier, M. Formal Methods in System Design (2002) 20: 7. https://doi.org/10.1023/A:1012952311559
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:99808
Collection:CaltechAUTHORS
Deposited By: Tony Diaz
Deposited On:12 Nov 2019 22:53
Last Modified:16 Nov 2021 17:49

Repository Staff Only: item control page