Decision procedures for algebraic data types with abstractions
Decision procedures for algebraic data types with abstractions
复制标题
DOI：
10.1145/1706299.1706325
复制
发表时间：
2010-01
期刊：
影响因子：
--
通讯作者：
Philippe Suter;Mirco Dotta;Viktor Kunčak
中科院分区：
文献类型：
--
作者：
Philippe Suter;Mirco Dotta;Viktor Kunčak
我们描述了一系列决策过程，这些过程扩展了递归代数数据类型（术语代数）上无量词约束的决策过程，以支持递归抽象函数。我们的抽象函数是变形（术语代数同态），将代数数据类型值映射到其他可判定理论（例如集合、多重集、列表、整数、布尔值）中的值。我们的决策程序族的每个实例都是健全的；我们在抽象函数上确定了一个广泛适用的多对一条件，这意味着完整性。我们的决策过程的完整实例包括以下正确性陈述：1）函数数据结构实现满足递归指定的不变量，2）此类数据结构符合以集合、多重集、列表、大小或高度给出的契约，3）公式（或 lambda 项）抽象语法树的转换以指定方式更改自由变量集。
We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term algebra homomorphisms) mapping algebraic data type values into values in other decidable theories (e.g. sets, multisets, lists, integers, booleans). Each instance of our decision procedure family is sound; we identify a widely applicable many-to-one condition on abstraction functions that implies the completeness. Complete instances of our decision procedure include the following correctness statements: 1) a functional data structure implementation satisfies a recursively specified invariant, 2) such data structure conforms to a contract given in terms of sets, multisets, lists, sizes, or heights, 3) a transformation of a formula (or lambda term) abstract syntax tree changes the set of free variables in the specified way.