Information Technology Reference
In-Depth Information
Note that
List
is true, i.e. an empty list is rep-
resented by void. Similar separation and interference properties as the ones for
Path
can be proved for
List
.
To prove the correctness of the annotated in-place list reversal algorithm listed
in Figure 4, we use standard Hoare-style reasoning. The annotations have type
Asrt
(
)(
o
,
h
)
is true iff
void
?(
)
null
o
:[
Object
v
⊥
,
Heap
⊥
→
]
bool
and a Hoare-triple has the following meaning
for
P
,
Q
:
Asrt
and
S
:
Stmt
:
∀
(
o
:
Object
v
⊥
,
h
:
Heap
⊥
):
P
(
o
,
h
)
⇒
Q
(
o
,
S
(
o
,
h
))
{
P
}
S
{
Q
}
=
)
distribute over the connectives. So, the actual work to verify the correctness
of the list reversal algorithm amounts to simplifying expressions of the form
(
g
List
(
o
,
h
As can be seen in Figure 4, the current object
o
and the updated heap
S
. By expanding the definitions of dot and as-
signment, this can be brought into the form of
List
(
l
)(
o
,
(
))(
o
,
(
:=
e
2
)(
o
,
h
))
l
e
1
f
p
,
h
))
,on
which the separation and interference rules for the
List
abstraction can be
applied.
(
:=
)(
f
q
{ λ
(
o
,
h
)
:
¬
bottom_or_void?
(
o
,
h
)
∧
a
List
(
As
)(
o
,
h
)
}
b:
=
void
;
WHILE
(
λ
(
o
,
h
)
:
¬
void?
(
a
(
o
,
h
)))
DO
{ λ
(
o
,
h
)
:
¬
bottom_or_void?
(
o
,
h
)
∧
∃
(
as
,
bs : list
[
Object
])
:
(
a
List
(
as
))(
o
,
h
)
∧
(
b
List
(
bs
))(
o
,
h
)
∧
disjoint?
(
as
,
bs
)
∧
append
(
reverse
(
as
),
bs
)
=
reverse
(
As
)
}
tmp :
=
a
;
a:
=
a
next
;
tmp
next :
=
b
;
b:
=
tmp
;
OD
{ λ
(
o
,
h
)
:
¬
bottom_or_void?
(
o
,
h
)
∧
(
b
List
(
reverse
(
As
)))(
o
,
h
)
}
Fig. 4.
In-place list reversal
5.3 Other Data Structures
The linearised specification approach exemplified in the previous two sections
can also be applied to other recursive data structures. Consider for example
binary trees that store a value in each node:
binary_tree
[
σ
]
:
TYPE
=
{
leaf
,
node
(
v:
σ
,
l
,
r : binary_tree
)}
It is straightforward to define a predicate
get_node
(
bt : binary_tree
[
σ
],
path : list
[
Name
],
v:
σ
)
: bool
Search WWH ::
Custom Search