Adding Records to Alloy

• Type: Article in International Conference Proceedings Book
• Date: 2023

Authors

Brunel, J (Author) Other; Chemouil, D (Author) Other; Cunha, A (Author) Other; Macedo, N (Author) FEUP

Conference proceedings International

Title: RIGOROUS STATE-BASED METHODS, ABZ 2023

Pages: 212-219

9th International Conference on Rigorous State-Based Methods (ABZ)

Nancy, FRANCE, MAY 30-JUN 02, 2023

Indexing

ISI Web of Knowledge - 1 Citation

Scopus

Other information

Authenticus ID: P-00Y-CCN

DOI: 10.1007/978-3-031-33163-3_16

Abstract (EN): 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 8