Go backward to
Proof of Fairness
Go up to
Top
Go forward to
Formal Specification
Hiding Variables
A simple processor/memory interface:
Processor issues
read
and
write
operations executed by memory.
Three interface registers:
op
: set by processor to indicate operation, reset by memory after operation.
adr
set by processor to indicate memory address to be read or written.
val
set by processor to indicate value to be written, set by memory to return result of
read
.
Specification
Phi
:
memory
(
n
) current value of location
n
.
Address
set of legal address.
MemVal
set of possible memory values.
Action
A
(
m
,
v
) assignment
memory
(
m
):=v.
Processor actions
R
proc
,
W
proc
.
Memory responses
R
mem
,
W
mem
.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998