The Temporal Logic of Actions II

Wolfgang Schreiner
Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria
  • Proving Simple Program Properties
  • Invariance Properties
  • Example: Type Correctness
  • Proof
  • General Invariance Proofs
  • More About Invariance Proofs
  • Eventuality Properties
  • Example
  • Other Properties
  • Another Example
  • The Formula Psi
  • The Next-State Relation
  • The Fairness Requirement
  • Proving Psi Implements Phi
  • Proof of Fairness
  • Hiding Variables
  • Formal Specification
  • Formal Specification (Contd)
  • Quantification over Flexible Variables
  • Quantification over Flexible Variables
  • Quantification in TLA
  • Refinement Mappings
  • A Simple Cached Memory
  • A Simple Cached Memory (Contd)
  • Formal Specification
  • Refinement Mappings
  • Summary
  • References
    • Wolfgang.Schreiner@risc.uni-linz.ac.at
    Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine