Go backward to Invariance Properties Go up to Top Go forward to Proof

Example: Type Correctness

• Type declarations in TLA:
  • Invariance property assuring that program variables are always from certain domain.
  • Phi => always T
• natural x, y
  • T <=> (x in Nat) and (y in Nat).
• Must prove:
  • Init_Phi => T
    T and [A]_{<x, y>} => T'
• Then we know:
  • Phi
    => Init_Phi and [A]_{<x, y>}
    => T and always [A]_{<x, y>}
    => always T