Program Composition in Isabelle/UNITY

11 years 4 months ago
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.
Sidi O. Ehmety, Lawrence C. Paulson
Added 15 Jul 2010
Updated 15 Jul 2010
Type Conference
Year 2002
Where IPPS
Authors Sidi O. Ehmety, Lawrence C. Paulson
Comments (0)