The Temporal Logic of Actions II

RISC-Linz logo

Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC-Linz)
Johannes Kepler University, A-4040 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

  • Author: Wolfgang Schreiner
    Last Modification: May 14, 1998

    [Up] [RISC-Linz] [University] [Search]