Bounded Relational Analysis of Free Data Types

In this paper we report on our first experiences using the relational analysis provided by the Alloy tool with the theorem prover KIV in the context of specifications of freely generated data types. The presented approach aims at improving KIV’s performance on first-order theories. In theorem proving practice a significant amount of time is spent on unsuccessful proof attempts. An automatic method that exhibits counter examples for unprovable theorems would offer an extremely valuable support for a proof engineer by saving his time and effort. In practice, such counter examples tend to be small, so usually there is no need to search for big instances. The paper defines a translation from KIV’s recursive definitions to Alloy, discusses its correctness and gives some examples.