2025/11/24 by Cunha, Alcino, Macedo, Nuno
#D.2.1 #D.2.4 #D.2.5 #FOS: Computer and information sciences #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2511.19177
This paper proposes a technique to help choose the best formal specification candidate among a set of alternatives. Given a set of specifications, our technique generates a suite of test cases that, once classified by the user as desirable or not, narrows down the set of candidates to at most one specification. Two alternative solver-based algorithms are proposed, one that generates a minimal test suite, and another that does not ensure minimality. Both algorithms were implemented in a prototype that can be used generate test suites to help choose among alternative Alloy specifications. Our evaluation of this prototype against a large set of problems showed that the optimal algorithm is efficient enough for many practical problems, and that the non-optimal algorithm can scale up to dozens of candidate specifications while still generating reasonably sized test suites.