Ulrich Geilmann

Karlsruhe Institute of Technology, Diplomarbeit, 2011

Alloy is a declarative specification language suitable for modeling structurally rich systems. It provides a relational first-order logic augmented with built-in operators for transitive closure, set cardinality, and integer arithmetics. The Analyzer automatically analyzes Alloy models by bounding the size of the modeled system.  Therefore, although capable of finding counterexamples, it cannot prove the model correct. In this thesis, an interactive first-order theorem prover, namely the KeY system, is used to provide such proving capability.
Alloy specifications are translated to KeY's first-order logic. For this purpose, a relational first-order theory is defined that resembles the relational calculus offered by Alloy, and supports most of the language features including all relational, set, and numerical operators. Unlike the Analyzer that bounds the size of a model's instances, our translation allows instances to be infinite. We prove that our translation is correct for the Alloy kernel, a subset of the Alloy language for which a formal semantics is available.
A translated Alloy model is loaded in the KeY system for proving. KeY's automatic proof search strategy is extended to allow efficient relational reasoning. We evaluate our approach by several experiments. As a case study, we prove Dijkstra's solution to the dining philosophers problem.