Synthesizing Test Cases for Narrowing Specification Candidates
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914169271353344 |
|---|---|
| author | Cunha, Alcino Macedo, Nuno |
| author_facet | Cunha, Alcino Macedo, Nuno |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_19177 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Synthesizing Test Cases for Narrowing Specification Candidates Cunha, Alcino Macedo, Nuno Software Engineering D.2.1; D.2.4; D.2.5 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. |
| title | Synthesizing Test Cases for Narrowing Specification Candidates |
| topic | Software Engineering D.2.1; D.2.4; D.2.5 |
| url | https://arxiv.org/abs/2511.19177 |