When & Where:
12:30pm, Friday, March 28, 2003, Room 400 AKW
Abstract:
Compositional reasoning involves, among other things, the ability to prove that a system satisfies its specification from the specifications of its components, as opposed to their implementations. To be successful, this approach requires specifications to be expressed in terms of operators that enjoy good compositional properties. In this talk, we look at some UNITY-like operators for specification from the point of view of compositionality. In passing, UNITY's (infamous) Substitution Axiom is discussed. We also consider compositional issues in related formalisms like TLA, and also from a more abstract point of view, independent from the underlying notation.