Information Technology Reference
In-Depth Information
(a portion of) the heap affects the corresponding abstract model. This comple-
ments local reasoning. In this paper we focus on the effects of assignments to
abstract models. We present our work in the setting of a core language, inspired
by Meyer's ideas for a semantics for the object-oriented language Eiffel [12].
Our framework allows us to express multidot field access expressions, mul-
tidot expressions for short, of the form f 1 ￿ f 2 ￿ ... ￿ f n . A multidot expression
consisting of a series of next -fields describes a path from the head of a list to
one of its elements. If we instantiate it with a series of left and right -fields
we can describe the path from the root of a binary tree to any node or leaf. In
general, a multidot expression describes a path on the heap where the elements
are connected by field accesses.
The main contribution of this paper is to provide a set of rules that precisely
describe the value of a multidot expression after an assignment, and to show
how these rules can be applied for verification of programs that manipulate
recursive data structures. The given rules are categorised into separation rules,
where the assignment has no effect on the multidot expression, and interference
rules, where the assignment does have effect on the multidot expression. We have
applied these rules to show the correctness of an in-place list reversal algorithm
by mapping each element of the list to a multidot expression. We also discuss
how to apply the same principles to other recursive data structures and we
make a comparison with the standard inductive approach. Our work has been
completely carried out in the theorem prover PVS [13].
This paper is organised as follows. Section 2 gives a short introduction to PVS
and introduces the notation. Section 3 defines the language we shall work with.
In Section 4 we present the rules that describe the effects an assignment can
have on a multidot expression and in Section 5 we apply these rules to prove
the correctness of a list reversal algorithm and we discuss the applicability to
other data structures. We compare the approach described in this paper with the
standard inductive approach and we give pointers for future work in Section 6.
Related work is discussed in Section 7 and conclusions are drawn in Section 8.
2
Preliminaries
PVS is based on higher-order logic with dependent types and predicate subtyp-
ing. Subtyping based on predicates makes type checking undecidable, so when
PVS cannot infer the desired type itself, it will generate a proof obligation. Its
intuitive syntax is reminiscent of functional languages like Haskell. For reasons
of presentation, we slightly simplify the actual PVS syntax. We will briefly in-
troduce the notation used in this paper.
Formulas are terms of type bool . We shall use the standard notation for
connectives (
). There is a conditional term
IF ϕ THEN M ELSE N ,forterms M, N of the same type.
Given the types σ, τ, σ 1 ,...,σ n , function types are written as
,
,
,
¬
), and for quantifiers (
,
[
σ
τ
]
and
record types as
[ lab 1 :
σ 1 ,..., lab n :
σ n ]
. Given the record types ρ 1 ,...,ρ m ,
labelled coproduct types are written as
{ lab 1 (
ρ 1 )
,..., lab m (
ρ m ) }
.Termsof
 
Search WWH ::




Custom Search