Go backward to
Formal Specification
Go up to
Top
Go forward to
Quantification over Flexible Variables
Formal Specification (Contd)
A
proc
<=>
op
= "ready"
and
op
' = "read"
and
adr
' in
Address
and
memory
' =
memory
A
proc
<=>
op
= "ready"
and
op
' = "write"
and
adr
' in
Address
and
val
' in
MemVal
and
memory
' =
memory
A
mem
<=>
op
= "read"
and
op
' = "ready"
and
val
' =
memory
(
adr
)
and
memory
' =
memory
A
mem
<=>
op
= "write"
and
op
' = "ready"
and
A
(
adr
,
val
)
Only interested in memory
interface
:
Behavior of
op
,
adr
,
val
.
Behavior of
memory
should be hidden.
exists
memory
:
Phi
.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998