AVAILABLE ELECTRONICALLY

"Composing Specifications"
Martin Abadi and Leslie Lamport
October 10, 1990.  90 pages

Authors' abstract

  A rigorous modular specification method requires a proof rule
  asserting that if each component behaves correctly in isolation,
  then it behaves correctly in concert with other components.  Such
  a rule is subtle because a component need behave correctly only when
  its environment does, and each component is part of the others'
  environments.  We examine the precise distinction between a system
  and its environment, and provide the requisite proof rule when modules
  are specified with safety and liveness properties.