Translating Alloy and Extensions to Classical B

Abstract

In this article, we introduce a denotational translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar. Each construct is translated into a semantically equivalent component of the B language. In addition to basic Alloy constructs, our approach supports integers, sequences and orderings. The translation is fully automated and our implementation can be used in ProB. We evaluate the usefulness by applying AtelierB and ProB to translated models, showing benefits for proof and constraint solving with integers and higher-order quantification.