Generating Specifications for Recursive Methods by Abstracting Program States

摘要

In this paper we present a novel approach to automatically generate sound specifications for recursive methods. These specifications can help prove the absence of undesired behavior, provide programmers with a foundation to build upon and help locate implementation bugs. Our approach is based on symbolic execution which we use to determine the states of re-entry and exit points. Prom these we generalize the necessary pre- and postconditions using techniques from abstract interpretation. The presented approach has been prototypically implemented by integration into a faithful and precise program logic for sequential Java programs.