Information Technology Reference
In-Depth Information
such that its least fixed point
μΦ
is the essence of dynamic semantics of
M
with its components
Σ
M
,E
M
and
r
M
, i.e.
μΦ
((
E
M
|
r
M
,Σ
M
,
∅
)) is the
Q
]]
ζ
U
is a notational variant of
state-update function [[
E
M
|
r
M
]] ( [[
E
|
yields
(
E
|
Q,
A
,ζ,U
)[BoS03]).
3.3 Verification
Denotational semantics, especially its fixed point theorem
μΦ
=
ν≥
0
Φ
ν
(
⊥
)
with its approximating semantics
Φ
ν
(
), is showing a way towards logic and
verification of ASMs in an area where ASM-literature is sparse, but where look-
ing at Algol-like programming might be helpful. ASM-logic is similar to dy-
namic logic [Har79] or algorithmic logic [Sal70, MiSa87]. Completeness results
in [BoS03] are presented only for hierarchical ASMs, i.e. ASMs without recur-
sions where call graphs have no cycles. The machines' analoga in Algol are so
called macro-programs the formal execution trees of which are finite.
In order to prove Algol-like programs with recursive procedures partially cor-
rect C.A.R.Hoare presented his proof rule for recursive procedures [Hoa71]. The
rule has, beside a conclusion and a premis, also a so called assumptions set.
It took quite a while until soundness and completeness results on Hoare's ex-
tended calculus came up. E.M.Clarke [Cla79] gave an intricate soundness proof
of Hoare's calculus, Clarke had not yet available an appropriate definition of
soundness of Hoare's proof rules with the decisive property: If all proof rules in
the calculus are sound then the whole calculus is sound.
1979 K.Apt and E.-R.Olderog [Apt79, Old79] independently came up with
the same idea how to define soundness of proof rules by help of approximating
semantics
Φ
ν
(
⊥
⊥
), specifically in the shape of a syntactical representation. It is
holding
r
M
]]
ν
=
Φ
ν
(
[[
E
M
|
⊥
)((
E
M
|
r
M
,Σ
M
,
∅
))
R
C
stat
ν
(
local
E
M
r
M
))]].
=[[
(
C
sta
ν
(
local
E
M
r
M
) is forming the formal execution tree (or a congruent version)
of
local
E
M
r
M
up to level
ν
. This means: Apply the copying process
C
stat
in
a simultaneous parallel manner
ν
-times to all rule calls outside any rule body
in a static scope manner, i.e. by avoiding name clashes by appropriate bound
renamings. In a next step
reduces the resulting tree by erazing all named
rules and replacing all remaining rule calls by
abort
.
E
R
abort
“
yields
|
the
bottom (undefined) update set which originates in
⊥
mentioned in the fixed point
theorem.
⊥
interpretes every rule call
E
|
r
(
t
1
,...,t
n
) by the totally undefined
state-update function.
Apt's and Olderog's inductive soundness proof of Hoare's proof rule for recur-
sive calls is a highlight in any course on program verification. We have mentioned
already in subsection 2.1 that there is no sound and relatively complete proof
calculus for the full static scope Algol60-language. This is holding for full Turbo
ASM as well. We have seen that such calculi are available only for certain sublan-
guages. It would be very illuminating to investigate how completeness results of
Search WWH ::
Custom Search