Information Technology Reference
In-Depth Information
Table 1.
Illustration of abstraction levels
The letters
v l
W
, i.e., it is a
valid workspace address.
x
is a variable of type word; it is assumed to be in the domain
of
.
adr
x
is the address of the memory cell allocated for
v
and
w
range over words;
v
additionally satises 1
x
.
E
5
(
ldl
;adr
x
)
SKIP
E
4
(
ldl
;adr
x
)
A
;
B
;
C
:=
x;
A
;
B
E
3
(
ldl
;v
)
A
;
B
;
C
:=
Wsp
(
v
)
;
A
;
B
E
2
(
ldl
;w
)
f
Index
(
Wptr
;w
)
2
Addr
g
;
A
;
B
;
C
:=
Mem
(
Index
(
Wptr
;w
))
;
A
;
B
E
1
(
ldl
)
f
Index
(
Wptr
;
Oreg
)
2
Addr
g
;
A
;
B
;
C
;
Oreg
:=
Mem
(
Index
(
Wptr
;
Oreg
))
;
A
;
B
;
0
E
0
(
ldl
)
f
Index
(
Wptr
;
Oreg
)
2
Addr
g
;
A
;
B
;
C
;
Oreg
:=
Mem
(
Index
(
Wptr
;
Oreg
))
;
A
;
B
;
0
total behavior resulting from starting
a b
with the rst instruction of
b
:
de
=
var IP
;[
Loaded
(
I
1
(
a;b
)
a b
)
^
IPAfter
(
a
)] ;
Run
;
end IP
:
:::
The outer block
var IP
end IP
hides the instruction pointer
IP
that is no
longer needed because the point of execution is symbolically represented from
now on. The assumption
3
[
Loaded
(
ab
)
^
IPAfter
(
a
)] ensures that
Run
is started
in a state where
a b
is loaded and the instruction pointer
IP
points just after
a
. The predicates
Loaded
(
u
)and
IPAfter
(
v
) are dened by
de
=
Loaded
(
u
)
jujl
P
^
h
Byte
(
Mem
;s
P
)
;:::;
Byte
(
Mem
;s
P
+
juj−
1)
i
=
Code
(
u
)
de
=
IP
=
IPAfter
(
v
)
s
P
+
jvj ;
where
l
P
are the start address and the length of the
program memory
,
i.e. that region of memory allocated to hold the program.
We also dene abstractions of the eect processes
s
P
and
E
0
(
instr
). These ensure
by a nal assertion and by taking the greatest lower bound over all possible
instruction sequences
that neither the loaded program (whatever it might
be) nor the position of execution is changed or, more precisely, that changes lead
to chaotic behavior:
a;b
de
=
^
a;b
E
1
(
instr
)
var IP
;[
Loaded
(
a b
)
^
IPAfter
(
a
)] ;
E
0
(
instr
);
;
end IP
:
3
For a predicate
,the
assumption
[
] is a process that | like the assertion
fg
| terminates immediately without state change if
holds but leads to miraculous
success otherwise. Formally, [
] is the predicate transformer [
](
)=(
)
).
f
Loaded
(
a b
)
^
IPAfter
(
a
)
g
Search WWH ::
Custom Search