Journal article
Reasoning about static and dynamic properties in alloy
Abstract
We study a number of restrictions associated with the first-order relational specification language Alloy. The main shortcomings we address are:---the lack of a complete calculus for deduction in Alloy's underlying formalism, the so called relational logic,---the inappropriateness of the Alloy language for describing (and analyzing) properties regarding execution traces.The first of these points was not regarded as an important issue during the …
Authors
Frias MF; Pombo CGL; Baum GA; Aguirre NM; Maibaum TSE
Journal
ACM Transactions on Software Engineering and Methodology, Vol. 14, No. 4, pp. 478–526
Publisher
Association for Computing Machinery (ACM)
Publication Date
October 2005
DOI
10.1145/1101815.1101819
ISSN
1049-331X