Compilation and Synthesis for Real-Time Embedded Controllers - Correct System Design: Recent Insights and Advances - page 256

Further Abstractions. Due to lack of space we can only briefly sketch the
remaining abstraction levels:

{ The third level I 3 replaces the memory variable Mem by an array Wsp (the

`workspace') of a xed length s W of the workspace pointer

is assumed and the workspace is mapped to the sequence of memory locations
just above

l W . A xed value

s W . The abstraction is based on a global assumption that this
memory region is disjoint from the program storage and contains only valid
addresses. It allows us to reason more easily about Transputer code that
accesses the memory via the usual workspace mechanism because reasoning
on this level need not reflect the mechanism by which the workspace is
mapped to memory. This is done only once while performing the abstraction.
{ The next level

4 replaces the workspace by a list of symbolic variables. The
set of introduced variables as well as their representation is described by a
dictionary

I

.
{ The nal level

I

5 hides the remaining registers A

; ;

C and EFlag and provides
a view in which only the communications via the links and the symbolic
variables are visible.

B

The choice of the abstraction levels is not accidental. They correspond very well
to the intuitive concepts used in informal reasoning about Transputer code and
can be interpreted as semantical analogues to increasingly abstract assembler
languages. A formally justied counterpart to the intuitive understanding of
each abstraction level is provided by an instruction theorem like Theorem 1,
special theorems for jumps and conditional jumps, and theorems about the single
instructions.

2.4 Incremental Specication of Code

We benet from the hierarchy of views to the Transputer's behavior when den-
ing the correctness relation between source and target programs. Consider as an
example a simple imperative programming language with syntactic categories
of programs, statements and expressions and assume that we are globally only
interested in the communication behavior of complete programs. Then it is sen-
sible to call a Transputer instruction sequence

m

correct code for a program prog

i

I 5 ( ";m ) MP ( prog ) ;

where MP ( prog ) is the meaning of prog interpreted in the space of processes, "

stands for the empty code sequence, and represents the empty dictionary.

Translation of statements, however, has to take representation of variables
into account. Therefore, a reasonable correctness condition relating a statement
stat to code

;

m must employ a non-trivial dictionary for the variables appearing

in stat . When comparing m with stat we cannot simply use the predicate given

by

5 (

I ";m ) MS ( stat ) ;