A relational framework for higher-order shape analysis
A relational framework for higher-order shape analysis
复制标题
高阶形状分析的关系框架
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
S. Jagannathan
中科院分区：
文献类型：
--
作者：
Gowtham Kaki;S. Jagannathan
我们建议在依赖类型系统中集成关系规范框架，该框架能够验证代数数据类型形状上的复不变式。我们的方法是基于这样的观察，即这种数据类型的结构属性通常可以自然地表示为在其定义中明显的递归结构上的归纳定义的关系。通过(抽象地)解释关系域中的构造函数应用程序，我们可以为各种复杂数据结构定义具有表现力的关系抽象，其结构和形状不变量可以被自动验证。我们的规范语言还允许为多态数据类型定义参数关系，从而实现高度可组合的规范，并自然地泛化为更高阶的多态函数。我们描述了一种算法，它将关系规范转换为一阶逻辑的可判定片段，可以由SMT求解器有效地执行。我们已经在一个名为CATALYST的类型检查器中实现了这些想法，该类型检查器包含在MLton SML编译器中。实验结果和案例分析表明，该验证策略是实用和有效的。
We propose the integration of a relational specification framework within a dependent type system capable of verifying complex invariants over the shapes of algebraic datatypes. Our approach is based on the observation that structural properties of such datatypes can often be naturally expressed as inductively-defined relations over the recursive structure evident in their definitions. By interpreting constructor applications (abstractly) in a relational domain, we can define expressive relational abstractions for a variety of complex data structures, whose structural and shape invariants can be automatically verified. Our specification language also allows for definitions of parametricrelations for polymorphic data types that enable highly composable specifications and naturally generalizes to higher-order polymorphic functions. We describe an algorithm that translates relational specifications into a decidable fragment of first-order logic that can be efficiently discharged by an SMT solver. We have implemented these ideas in a type checker called CATALYST that is incorporated within the MLton SML compiler. Experimental results and case studies indicate that our verification strategy is both practical and effective.