Sciweavers

Share
CADE
2008
Springer

Specification Predicates with Explicit Dependency Information

9 years 2 months ago
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.
Richard Bubel, Reiner Hähnle, Peter H. Schmit
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Richard Bubel, Reiner Hähnle, Peter H. Schmitt
Comments (0)
books