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

register values at dierent stages of execution; we dierentiate between them im-
plicitly by the places at which they appear in the formulas. The register updates
caused by ldc can be represented simply by a multiple assignment statement:

E 0 ( ldc ) A ; B ; C ; Oreg := Oreg ; A ; B ; 0 : (3)

This renement formula can be interpreted as an axiom on ldc 's behavior.
Comparing it with the Z-like schema above, the careful reader will notice that
incrementation of the instruction pointer is missing. We have decided to move
it consistently for all instructions to the fetch phase as this is slightly more
convenient for the following exposition.
The behavior of the other instructions can be captured by similar axioms.
This keeps the modularity of the description in [23]. Each instruction is de-
scribed separately by one (or more) formula, which leads in the abstractions to
short proofs for single instructions instead of one monolithic proof for the en-
tire instruction set. In addition, it allows to reason formally with only a partial
formalization of the instruction set; only the instructions actually used in the
compiler need be considered.
The axioms on

E 0 ( instr ) claim renement, not equality. This has a particular
benet: it allows to approximate the actual eect safely if it is not completely
known. As an example, let us consider the following axiom for the instruction
stl (store-local). Intutitively, stl stores the top value of the register mini-stack
to a certain location in the memory.

E 0 ( stl ) f Index ( Wptr ; Oreg ) 2 Addr g ;

Mem [

Index ( Wptr ; Oreg )] ; A ; B ; Oreg := A ; B ; C ; 0; C := ? :

Addr denotes the set of valid word addresses and contains only those addresses

for which memory is actually available. The assertion f Index ( Wptr ; Oreg ) 2

Addr g ensures that the inequality is trivial if the referenced memory address

Index ( Wptr ; Oreg ) is invalid. This means that the axiom doesn't tell how stl

behaves in this situation. The nice eect is that we must ensure, when reasoning
about correctness of code, that stl is not used under such circumstances as we
cannot otherwise show correctness.
The non-deterministic assignment C := ? captures that the contents of register
C after a stl location is left unspecied by the Transputer designers. Clearly,
the C register will contain a certain value but our axiom does not say which.
So any reasoning based on this axiom cannot rely on any specic assumption
about the nal value of C . Without the use of non-determinism and renement
we would be forced either to describe the eect of stl on the register C and
stl 's behavior when it accesses invalid addresses completely, or to work with
an idealized model. The rst solution is impractical as such information is not
available; the second solution might lead to unsafe reasoning.