Conjoining Specifications I

Wolfgang Schreiner
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria
  • Parallel Program Composition
  • Composed Specifications
  • Decomposing Complete Systems
  • Hierarchical Development
  • Refinement of Components
  • Decomposition of Proofs
  • Composing Open Systems
  • A Queue Process
  • Queue Specification
  • Reasoning about Composed Systems
  • Reasoning about Composed Systems
  • Reasoning about Composed Systems
  • TLA
  • Interleaving Representations
  • The Queue Example
  • TLA Specification of Queue
  • Implementation
  • Two Queues in Series
  • Specification
  • Conditional Implementation
  • Safety and Closure
  • Machine Closure
  • Closure and Hiding
  • Additional Temporal Operators
  • Additional Temporal Operators
  • Additional Temporal Operators
  • Further Propositions
  • References

  • Wolfgang.Schreiner@risc.uni-linz.ac.at
    Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine