Program Composition in Isabelle/UNITY

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.

• Type: Conference
• Year: 2002
• Where: IPPS
• Authors: Sidi O. Ehmety, Lawrence C. Paulson
• Keywords: Compositional Reasoning, Distributed And Parallel Computing, Existential, IPPS 2002, Mechanization