Go backward to Formal Specification
Go up to Top
Go forward to Summary
Refinement Mappings
- Refinement Mappings
- Prove: (exists ,...,: Psi)
(exists ,...,: Phi)
- Define state functions , ..., in terms of
the variables occuring in Psi.
- Prove Psi Phi.
- Phi := Phi(/, ...,
/).
- Mapping need not exist:
- Can prove: (exists sem, pc, pc: Psi)
Phi.
- Cannot prove: Phi
(exists sem, pc, pc: Psi)
- Cannot define state functions sem, pc,
pc in terms of and .
- Addition of auxiliary variables:
- (exists , : Phi)
(exists sem, pc, pc: Psi)
- Using auxiliary variables, refinement mappings can be always found.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine