Go backward to
Formal Specification
Go up to
Top
Go forward to
Summary
Refinement Mappings
Refinement Mappings
Prove: (
exists
x
1
,...,
x
m
:
Psi
)
=>
(
exists
y
1
,...,
y
n
:
Phi
)
Define state functions
y
1
, ...,
y
n
in terms of the variables occuring in
Psi
.
Prove
Psi
=>
Phi
.
Phi
:=
Phi
(
y
1
/
y
1
, ...,
y
n
/
y
n
).
Mapping need not exist:
Can prove: (
exists
sem
,
pc
1
,
pc
2
:
Psi
)
=>
Phi
.
Cannot prove:
Phi
=>
(
exists
sem
,
pc
1
,
pc
2
:
Psi
)
Cannot define state functions
sem
,
pc
1
,
pc
2
in terms of
x
and
y
.
Addition of auxiliary variables:
(
exists
h
,
p
:
Phi
hp
)
=>
(
exists
sem
,
pc
1
,
pc
2
:
Psi
)
Using auxiliary variables, refinement mappings can be always found.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998