Translating Alloy and Extensions to Classical B
Published in International Journal on Science of Computer Programming, 2020
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.
Sebastian Krings, Michael Leuschel, Joshua Schmidt, David Schneider and Marc Frappier. (2020). "Translating Alloy and Extensions to Classical B" International Journal on Science of Computer Programming. https://link.springer.com/chapter/10.1007/978-3-030-20652-9_9