Go backward to
Refinement Mappings
Go up to
Top
Go forward to
A Simple Cached Memory (Contd)
A Simple Cached Memory
Phi
<=>
Init
Phi
and
always
[
A
]
u
and
WF
u
(
A
).
Init
Phi
<=>
op
= "ready"
and
forall
n
in
Address
:
(
main
(
n
) in
MemVal
)
and
(
cache
(
n
) =
bottom
)
u
<=>
<
op
,
adr
,
val
,
main
,
cache
>
A
<=>
A
pro
or
A
pro
or
A
cch
or
A
cch
or
(
exists
m
in
Address
:
A
get
(
m
)
or
A
fl
(
m
))
A
<=>
A
pro
or
A
pro
or
(
A
get
(
adr
)
and
(
op
= "read"))
A
(
a
,
m
,
v
)
<=>
forall
n
in
Address
:
(
n
=
m
)
=>
(
a'
(
n
) =
v
)
and
(
n'
notequal
m
)
=>
(
a'
(
n
) =
a
(
n
))
A
pro
<=>
op
= "ready"
and
op
' = "read"
and
adr
' in
Address
and
Unchanged
<
main
,
cache
>
A
pro
<=>
op
= "ready"
and
op
' = "write"
and
adr
' in
Address
and
val
' in
MemVal
and
Unchanged
<
main
,
cache
>
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998