Specification Predicates with Explicit Dependency Information

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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Richard Bubel, Reiner Hähnle, Peter H. Schmitt
• Keywords: Automated Reasoning, CADE 2008, General Simplification Rules, Hidden Dependencies, Non-trivial Case Studies