Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions
Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions
复制标题
（共）归纳谓词、（共）代数数据类型和（共）递归函数的关系分析
DOI：
10.1007/s11219-011-9148-5
复制
发表时间：
2013
影响因子：
1.9
通讯作者：
Jasmin Christian Blanchette
中科院分区：
文献类型：
--
作者：
Jasmin Christian Blanchette
我们提出的技术应用有限的关系模型查找器的逻辑规范，涉及高层次的定义原则，如（共）归纳谓词，（共）代数datashees，（共）递归函数。与以前的工作，主要集中在代数datashees和限制出现的无界量词的公式，我们可以处理任意公式通过一个三值Kleene逻辑。这些技术构成了Isabelle/HOL的反例生成器Nitpick的基础。作为案例研究，我们认为公式归纳定义上下文无关的语法，AA树的功能实现，和一个coalgebraic列表数据类型。
We present techniques for applying a finite relational model finder to logical specifications that involve high-level definitional principles such as (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. In contrast to previous work, which focused on algebraic datatypes and restricted occurrences of unbounded quantifiers in formulas, we can handle arbitrary formulas by means of a three-valued Kleene logic. The techniques form the basis of the counterexample generator Nitpick for Isabelle/HOL. As case studies, we consider formulas about an inductively defined context-free grammar, a functional implementation of AA trees, and a coalgebraic list datatype.
登录
查看更多内容
使用 KIV 进行正式系统开发
DOI：
--
发表时间：
2000
期刊：
Fundamental Approaches to Software Engineering
影响因子：
--
作者：
M. Balser;W. Reif;G. Schellhorn;Kurt Stenzel;A. Thums
通讯作者：
A. Thums
代数数据类型的关系分析
DOI：
--
发表时间：
2005
期刊：
ESEC/FSE-13
影响因子：
--
作者：
Viktor Kunčak;D. Jackson
通讯作者：
D. Jackson
为什么我们不能在 HOL 中使用 SML 风格的数据类型声明
DOI：
10.1016/b978-0-444-89880-7.50042-5
发表时间：
1992
期刊：
J. Log. Comput.
影响因子：
--
作者：
Elsa L. Gunter
通讯作者：
Elsa L. Gunter
DOI：
10.1007/3-540-58156-1_11
发表时间：
1994
期刊：
ArXiv
影响因子：
--
作者：
Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
在 Isabelle/HOL 中查找终止证明的词典顺序
DOI：
--
发表时间：
2007
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
Lukas Bulwahn;Alexander Krauss;T. Nipkow
通讯作者：
T. Nipkow