A Formal Semantics for Isorecursive and Equirecursive State Abstractions
A Formal Semantics for Isorecursive and Equirecursive State Abstractions
复制标题
等递归和等递归状态抽象的形式语义
DOI：
10.1007/978-3-642-39038-8_6
复制
发表时间：
2013
影响因子：
3.6
通讯作者：
S. Drossopoulou
中科院分区：
文献类型：
--
作者：
Alexander J. Summers;S. Drossopoulou
静态程序验证和分析的方法通常支持规范中的递归谓词，以便推理递归数据结构。直观上，谓词实例代表其定义的完整展开；这是等递归解释。然而，当递归变得无界时，这种语义不适合静态验证。因此，大多数静态验证器会区分谓词实例及其相应的主体，同时提供在两者之间进行映射的工具；这就是等递归语义。虽然后一种解释通常在实践中实现，但在理论工作中通常只处理等递归语义。
在本文中，我们为 Chalice（一种基于隐式动态框架的验证方法）上下文中的递归定义提供了等递归和等递归形式语义。我们表明，这种形式化的开发需要解决几个微妙的问题，例如无限递归定义的可能性以及等递归语义正确反映使其易于实现的限制的需要。在隐式动态框架的背景下，这些问题仍然变得更具挑战性，其中依赖于堆的表达式的使用为正确的形式处理提供了进一步的陷阱。
Methodologies for static program verification and analysis often support recursive predicates in specifications, in order to reason about recursive data structures. Intuitively, a predicate instance represents the complete unrolling of its definition; this is the equirecursive interpretation. However, this semantics is unsuitable for static verification, when the recursion becomes unbounded. For this reason, most static verifiers differentiate 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 definitions in the context of Chalice, a verification methodology based on implicit dynamic frames. We show that development of such formalisations requires addressing several subtle issues, such as the possibility of infinitely-recursive definitions and the need for the isorecursive semantics to correctly reflect 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.