Are anamorphisms reasonable abstractions?

In calculational derivations of pointer algorithms the concept of a reasonable abstraction function has proved to be of central importance. A function from pointer structures to some other domain iscalledreasonableif it only depends on the reachable part of the store. Forreasonable functions we can reduce questions about invariance of certainparts of objects to an analysis of (non-)reachability in the pointer structure. In this way we can prove a number of transformation laws once and for all types of pointer structures. In the present paper we show that all abstraction functions with an anamorphic recursive definition are reasonable, so that our laws apply for them. The approach copes also with cyclic strctures; among others, we give abstraction functions for cyclic lists and threaded trees. By tuning the degree of abstraction we can give simple specifications for routines that are to update pointer structures in situ