Conjoining Specifications II

Wolfgang Schreiner
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria
  • Decomposing a Complete Specification
  • Component Specification
  • Queue Component
  • Queue Component
  • Conjoining Specifications
  • Proposition
  • Two Queues in Series
  • The Decomposition Theorem
  • Decomposition Theorem
  • Verifying the Hypotheses
  • Verifying the Hypotheses
  • GCD Example (Contd)
  • The General Theorem
  • Composing Assumption/Guarantee Specifications
  • The Composition Theorem
  • Corollary
  • Queue Example
  • Queue Example
  • Conclusion
  • References

  • Wolfgang.Schreiner@risc.uni-linz.ac.at
    Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine