Formally specifying the behavior of pointer-based programs as a prerequisite of their computer-aided verification is difficult and error-prone. One has not only to specify the shape of the data structures, but also the properties that capture the desired level of program correctness. While the former task can be standardized by predicate libraries that describe typical shapes, the latter is ad hoc; so, one may easily miss information that is crucial for the subsequent verification.

To overcome this problem, this paper presents a system where the user annotates the program by a precondition and postcondition that express (in separation logic) only the shape of the data structure. The system completes this specification by adding preconditions for memory safety and relational constraints that link the post-state to the pre-state and capture its properties. For this, the system computes by a forward analysis of the program the postcondition in the form of a constraint abstraction, a recursively defined predicate from which the nonshape properties are then extracted. Finally, a fixpoint solver derives the nonrecursive solution.

The paper describes the core ideas by using various illustrative examples, which are accessible to the nonexpert. The main part of the paper is dedicated to the technical details, which culminate in the soundness and termination of the analysis. Finally, experimental results demonstrate which properties can be derived for various list processing programs. While the presented semiautomatic approach to formal specification is still in its early stages, it provides a lot of potential for extension to more general programs and properties.