Go backward to A Simple Cached Memory (Contd)
Go up to Top
Go forward to Refinement Mappings
Formal Specification
- Correctness statement:
- (exists main, cache: Psi)
(exists memory: Phi)
- Proof:
- memory() if cache() =
bottom
then main() else cache()
- Psi Phi(memory/memory)
- "Concrete" state function memory implements "abstract"
variable memory.
- Cached memory still abstract:
- No particular cache maintenance policy is specified.
- Given a concrete caching algorithm, it has to be proved that
it implements the simple cached memory.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine