Information Technology Reference
In-Depth Information
5
(
since | inherited from
Run
|
) does not terminate. (For complete pro-
grams this problem does not arise: we assume that programs stop on termination
which can be achieved by a
stopp
instruction in
I
";m
). The main purpose of termi-
nation of
stat
is to transfer control to its sequential successor. Therefore, we do
not expect that the machine stops after execution of
m
m
but rather that control is
transferred to the code just following
. Formalizing this idea we use the follow-
ing predicate as notion of correct implementation of statements:
m
m
implements
stat
w.r.t. dictionary
,
CS
(
m;
stat
;
) for short, i
5
(
5
(
I
a;m b
)
MS
(
stat
);
I
am;b
)
;
for all code sequences
. A correctness predicate for expression translation must
refer to the more concrete view
a;b
4
because correct expression code is expected
to leave the expression's value in register
A
that is not visible on Level 5.
Having dened correctness predicates, we establish for each source language
constructor a theorem that shows how correct code for the composed construct
can be obtained from correct code of the components. From a comprehensive set
of such theorems a code generator program can be implemented without further
semantic consideration. As a rst example we present the theorem for sequential
composition here; further examples can be found in Sect. 2.6.
Not surprisingly, the sequential composition
seq
(
stat
1
;
I
stat
2
)oftwostate-
ments
stat
1
and
stat
2
can simply be implemented by concatenating machine
code implementing
stat
1
and
stat
2
.
Theorem 3 (Sequential composition translation).
Suppose
CS
(
m
1
;
stat
1
;
)
CS
m
2
;
and
(
stat
2
;
)
hold. Then
CS
(
m
1
m
2
;
seq
(
stat
1
;
stat
2
)
;
)
.
The proof is by a little calculation that applies to arbitrary code sequences
a
and
; of course, sequential composition in the source language corresponds to
the sequential composition operator ; of the meta-language:
b
5
(
I
a;m
1
m
2
b
)
CS
m
1
;
stat
1
;
[
(
)]
5
(
MS
(
stat
1
);
I
am
1
;m
2
b
)
CS
m
2
;
stat
2
;
[
(
)]
5
(
MS
(
stat
1
);
MS
(
stat
2
);
I
am
1
m
2
;b
)
=
[Denition of semantics of
seq
]
5
(
MS
(
seq
(
stat
1
;
stat
2
)) ;
I
a m
1
m
2
;b
)
:
The simplicity of this proof, which looks almost too straightforward to be of
interest, stems from the use of the adequate abstraction level. If we had dened
CS
with direct reference to the Transputer base model (which is easily done
by unfolding the denition of
5
) the proof would be far more complex as all
invariants that are kept by the code had to be explicitly treated. Now they are
treated incrementally during the derivation of the abstraction levels. Moreover,
we would not have such a clear way of speaking about the control point but had
to refer to its coding in the instruction pointer.
I
Search WWH ::
Custom Search