Summers, Alexander J.
Rights / licenseIn Copyright - Non-Commercial Use Permitted
Methodologies for static program verication and analysis often support recursive predicates in specications, in order to reason about recursive data structures. Intuitively, a predicate instance represents the complete unrolling of its denition; this is the equirecursive interpretation. However, this semantics is unsuitable for static veri- cation, when the recursion becomes unbounded. For this reason, most static veriers dierentiate between, e.g., a predicate instance and its corresponding body, while providing a facility to map between the two; this is the isorecursive semantics. While this latter interpretation is usually implemented in practice, only the equirecursive semantics is typically treated in theoretical work. In this paper, we provide both an isorecursive and an equirecursive formal semantics for recursive denitions in the context of Chalice, a veri cation methodology based on implicit dynamic frames. We show that development of such formalisations requires addressing several subtle issues, such as the possibility of innitely-recursive denitions and the need for the isorecursive semantics to correctly re ect the restrictions that make it readily implementable. These questions are made more challenging still in the context of implicit dynamic frames, where the use of heap-dependent expressions provides further pitfalls for a correct formal treatment Show more
External linksFull text via SFX
Journal / seriesTechnical report / ETH Zurich, Department of Computer Science
SubjectHOARE LOGIC (MATHEMATICAL LOGIC); RECURSION THEORY (MATHEMATICS); VERIFICATION (SOFTWARE ENGINEERING); HOARESCHE LOGIK (MATHEMATISCHE LOGIK); VERIFIKATION (SOFTWARE ENGINEERING); SEMANTIK VON PROGRAMMIERSPRACHEN + SYNTAX VON PROGRAMMIERSPRACHEN; SEMANTICS OF PROGRAMMING LANGUAGES + SYNTAX OF PROGRAMMING LANGUAGES; REKURSIONSTHEORIE (MATHEMATIK); SEMANTICS OF LOGICAL LANGUAGES (MATHEMATICAL LOGIC); SEMANTIK LOGISCHER SPRACHEN (MATHEMATISCHE LOGIK)
Organisational unit03653 - Müller, Peter
02150 - Departement Informatik / Department of Computer Science
NotesTechnical Reports D-INFK.
MoreShow all metadata