Theory Exploration for Programs and Proofs

Sammanfattning: We have built two theory exploration systems, Cohipster and RoughSpec . Theory exploration is a method of automatically conjecturing properties about the functions and structures that appear in a computer program or a formalization of a mathematical theory. Cohipster is a theory exploration system that discovers equational lemmas about corecursive functions in Isabelle/HOL and automatically searches for coinductive proofs for them. Coinduction and corecursion are the mathematical duals of induction and recursion and allow the specification of potentially infinite structures such as streams, and functions that operate on such structures. Cohipster is the first system to automatically discover and prove coinductive lemmas, and its design required the development of techniques for testing infinite structures as well as for automating coinductive proofs. RoughSpec is a template-based theory exploration system for Haskell programs. RoughSpec allows users to specify what kinds of properties they are interested in finding by using templates. A template is an expression describing a family of properties, such as distributivity or commutativity, that have a particular shape. Limiting the search space to specific shapes of properties makes theory exploration more targeted and tractable than previous methods.