Published in

Proceedings 16th International Parallel and Distributed Processing Symposium

DOI: 10.1109/ipdps.2002.1016620

Links

Tools

Export citation

Search in Google Scholar

Program composition in Isabelle/UNITY

Journal article published in 2002 by Sidi O. Ehmety, Lawrence C. Paulson
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Green circle
Postprint: archiving allowed
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

Abstract

We describe the mechanization of recent examples of compositional reasoning, due to Charpentier and Chandy [4]. The examples illustrate a new theory for composition proposed by Chandy and Sanders [2, 3], based on the so-called existential and universal properties. We show that, while avoiding hand proof mistakes, a such compositional reasoning can be mechanized quite straightforwardly. We also present the mechanization of some theoretical results [5] concerning existential properties and their relation with the guarantees concept. The result is a new module added to the existing Isabelle/UNITY theory for composition.