Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive definitions. The definition of these symbols often depends implicitly on the value of other locations such as fields that are not stated explicitly as arguments. These hidden dependencies make the verification process substantially more difficult. In this paper we develop a framework that makes dependency on locations explicit. This allows to define general simplification rules that avoid unfolding of predicate definitions in many cases. A number of non-trivial case studies show the usefulness of the concept.

@inproceedings{BubelHaehnleSchmitt2008,
  author       = {Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt},
  title        = {Specification Predicates with Explicit Dependency Information},
  editor       = {Bernhard Beckert},
  booktitle    = {Proceedings, 5th International Verification Workshop (VERIFY'08)},
  volume       = {372},
  series       = {CEUR Workshop Proceedings},
  pages        = {28--43},
  publisher    = {CEUR-WS.org},
  year         = {2008}
}