Automating Algebraic Specifications of Non-freely Generated Data Types

Non-freely generated data types are widely used in cases studies carried out in the theorem prover KIV. The most famous examples are stores, sets and arrays. We present an automatic method that generates finite counter examples for wrong conjectures and therewith offers a valuable support for proof engineers saving their time otherwise spent on unsuccessful proof attempts. The approach is based on the finite model finding and uses Alloy Analyzer to generate finite instances of theories in KIV. Most definitions of functions or predicates on infinite structures do not preserve the semantics if a transition to arbitrary finite substructures is made. We propose the constraints which should be satisfied by the finite substructures, identify a class of amenable definitions and present a practical realization using Alloy. The technique is evaluated on the library of basic data types as well as on some examples from case studies in KIV.