The UNITY Programming Logic

Wolfgang Schreiner
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria
  • The UNITY Programming Logic
  • Assignment Statements
  • Quantified Assertions
  • A Model of Program Execution
  • Application of Execution Model
  • Fundamental Concepts
  • Unless
  • Special Cases of Unless
  • Special Cases of Unless
  • Ensures
  • Leads-to
  • Fixed Point
  • An Example
  • Proofs
  • Invariant Proof
  • Fixed Point Proof
  • Fixed Point Proof
  • Proof of Ensure Relations
  • Proof of Unless Relations
  • References
    • Wolfgang.Schreiner@risc.uni-linz.ac.at
    Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine