2024/11/24 by Dancy, Ryan, Day, Nancy A., Zila, Owen +2
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2411.15978
Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the Kodkod library as a back-end for finite model finding. Kodkod translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present Portus, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the Fortress library, creating an alternative back-end for the Alloy Analyzer. Fortress converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of Portus with Kodkod on a corpus of 64 Alloy models written by experts. Our method is fully integrated into the Alloy Analyzer.