An abstract account of composition

Martín Abadi, Stephan Merz
We present a logic of specifications of reactive systems. The logic is independent of particular computational models, but it captures common patterns of reasoning with assumption-commitment specifications. We use the logic for deriving proof rules for TLA and CTL* specifications.
© Springer-Verlag
Available as:  gzip'ed Postscript 
  author =    "Mart\'{\i}n Abadi and Stephan Merz",
  title =     "An Abstract Account of Composition",
  year =      1995,
  editor =    "J. Wiedermann and P. Hajek",
  volume =    969,
  booktitle = "Mathematical Foundations of Computer Science",
  series =    "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  address =   "Prague, Czech Republic",
  pages =     "499--508"

Stephan Merz