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
(
m
)
<=>
if
cache
(
m
) =
bottom
then
main
(
m
)
else
cache
(
m
)
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.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998