Abstract
In this paper, we introduce a 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 and orderings. The translation is fully automated by the tool “Alloy2B”. We evaluate the usefulness by applying AtelierB and ProB to the translated models, and show benefits for proof and solving with integers and higher-order quantification.
Cite
CITATION STYLE
Krings, S., Schmidt, J., Brings, C., Frappier, M., & Leuschel, M. (2018). A translation from alloy to B. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10817 LNCS, pp. 71–86). Springer Verlag. https://doi.org/10.1007/978-3-319-91271-4_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
