Information Technology Reference
In-Depth Information
Similarly, the eect of
stl
(
, moving
B
's
value to
A
,
C
's value to
B
, and an unspecied value to
C
, can be described by
x
), writing
A
's contents to variable
x
de
=
E
(
stl
(
x
))
x;
A
;
B
:=
A
;
B
;
C
;
C
:= ?
;
where
C
:= ? denotes the nondeterministic choice between all possible assign-
ments to
C
. To specify a machine by a high level program is of course not a
new idea; it already underlies the concept of micro-programming [47], for in-
stance. Such descriptions can also be used as starting point for hardware design
[27,10,19] and thus provide a good interface to lower levels of abstraction.
If semantics of machine instructions is captured by imperative program frag-
ments, renement algebra [21], which provides semantics-preserving or rening
program transformation rules, can be used to show that certain machine instruc-
tion sequences implement certain source programs. The following calculation
proves, for example, that the code sequence
, assumed to have
the same meaning as the sequential composition of the eects
h
ldc
(1)
;
stl
(
x
)
i
E
(
ldc
(1)) and
E
:= 1; for the moment the
additional eect on the accumulator
C
is taken to be irrelevant:
(
stl
(
x
)), is correct target code for the assignment
x
E
(
ldc
(1)) ;
E
(
stl
(
x
))
=
[Denitions above]
A
;
B
;
C
:= 1
;
A
;
B
;
x;
A
;
B
:=
A
;
B
;
C
;
C
:= ?
=
[(Combine-assign), (Identity-assign)]
x;
;
;
C
:= 1
;
;
;
B
;
C
:= ?
A
B
A
B
=
[(Cancel-assign), (Identity-assign)]
x
:= 1 ;
C
:= ?
:
In this proof we have used the following three assignment laws where
x
and
y
stand for disjoint lists of variables,
e
and
f
for lists of expressions of correspond-
ing type, and
f
[
e=x
] denotes substitution of
e
for
x
in expression
f
.
(Identity-assign)
(
x
:=
e
)=(
x;y
:=
e;y
)
x
e
x
f
x
f
e=x
(Combine-assign)
(
:=
;
:=
)=(
:=
[
])
(Cancel-assign)
(
x;y
:=
e;f
;
y
:= ?) = (
x
:=
e
;
y
:= ?)
The above calculation illustrates a basic idea of our approach to compiler
verication: to use an imperative meta-language and renement laws as proposed
by Hoare [20,22]. We write
for the renement relation; intuitively
P Q
means
in every context.
1
1
Due to lack of space we cannot present a formal denition of the meta-language
in this article. For the purpose of this overview an informal understanding is suf-
cient. Let us just mention that the imperative meta-language is interpreted by
predicate transformers in the tradition of Dijkstra's wp-calculus [12] and the rene-
ment calculus [34,5,32] but extended to communicating programs. For performing
the abstractions we use a variant of the data renement theory of Back [4], Gardiner
& Morgan [16], and Morris [35]. Details can be found in the monograph [37].
that
P
is better than
Q
in serving every purpose served by
Q
Search WWH ::
Custom Search