Translating Alloy and Extensions to Classical B


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.

In Science of Computer Programming, Elsevier
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.