Go backward to
Hiding Variables
Go up to
Top
Go forward to
Formal Specification (Contd)
Formal Specification
Phi
<=>
Init
Phi
and
always
[
A
]
w
and
WF
w
(
A
mem
)
Init
Phi
<=>
op
= "ready"
and
forall
n
in
Address
:
memory
(
n
) in
MemVal
A
<=>
A
mem
or
A
proc
or
A
proc
A
mem
<=>
A
mem
or
A
mem
w
<=>
<
op
,
adr
,
val
,
memory
>
A
(
m
,
v
)
<=>
forall
n
in
Address
:
(
n
=
m
)
=>
(
memory
(
n
)' =
v
)
and
(
n
notequal
m
)
=>
(
memory
(
n
)' =
memory
(
n
))
Fairness condition:
Memory eventually responds to each request.
Processor need not issue requests.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998