Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89469
Título: | Adding records to alloy |
Autor(es): | Brunel, Julien Chemouil, David Cunha, Alcino Macedo, Nuno |
Palavras-chave: | Alloy Formal specification Model checking |
Data: | 2023 |
Editora: | Springer, Cham |
Revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Citação: | Brunel, J., Chemouil, D., Cunha, A., Macedo, N. (2023). Adding Records to Alloy. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds) Rigorous State-Based Methods. ABZ 2023. Lecture Notes in Computer Science, vol 14010. Springer, Cham. https://doi.org/10.1007/978-3-031-33163-3_16 |
Resumo(s): | Records are a composite data type available in most programming and specification languages, but they are not natively supported by Alloy. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures. This paper proposes a conservative extension to the Alloy language to support record signatures. Uniqueness and completeness is imposed on the atoms of such signatures, while still supporting Alloy’s flexible signature hierarchy. The Analyzer has been extended to internally expand such record signatures as partial knowledge for the solving procedure. Evaluation shows that the proposed approach is more efficient than commonly used idioms. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/89469 |
ISBN: | 978-3-031-33162-6 |
e-ISBN: | 978-3-031-33163-3 |
DOI: | 10.1007/978-3-031-33163-3_16 |
ISSN: | 0302-9743 |
Versão da editora: | https://link.springer.com/chapter/10.1007/978-3-031-33163-3_16 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
ABZ23a.pdf | 406,09 kB | Adobe PDF | Ver/Abrir |