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
- natural ,
- ( in Nat) and (
in Nat).
- Must prove:
- Init
and [A]
- Then we know:
- Phi
Init
and [A]
and always [A]
always
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine