Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions

摘要

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.