In this paper we investigate the existence of a deductive verification
method based on a logic that describes pointer aliasing. The main idea
of such a method is that the user has to annotate the program with loop
invariants, pre- and post-conditions. The annotations are then automatically
checked for validity by propagating weakest preconditions and verifying
a number of induced implications. Such a method requires an underlying
logic which is decidable and has a sound and complete weakest precondition
calculus. We start by presenting a powerful logic ({\bf wAL}) which can
describe the shapes of most recursively defined data structures (lists,
trees, etc.) has a complete weakest precondition calculus but is undecidable.
Next, we identify a decidable subset ({\bf pAL}) for which we show closure
under the weakest precondition operators. In the latter logic one loses
the ability of describing unbounded heap structures, yet bounded
structures can be characterized up to isomorphism. For this logic
two sound and complete proof systems are given, one based on natural
deduction, and another based on the effective method of analytic tableaux.
The two logics presented in this paper can be seen as extreme values in a
framework which attempts to reconcile the naturally oposite goals of
expressiveness and decidability.
