Towards an Operational Semantics for Alloy

Abstract. The Alloy modeling language has a mathematically rigorous denotational semantics based on relational algebra. Alloy specifications often represent operations on a state, suggesting a transition-system semantics. Because Alloy does not intrinsically provide a notion of state, however, this interpretation is only implicit in the relational-algebra semantics underlying the Alloy Analyzer. In this paper we demonstrate the subtlety of representing state in Alloy specifications. We formalize a natural notion of transition semantics for state-based specifications and show examples of specifications in this class for which analysis based on relational algebra can induce false confidence in designs. We characterize the class of facts that guarantees that Alloy’s analysis is sound for statetransition systems, and offer a sufficient syntactic condition for membership in this class. We offer some practical evaluation of the utility of this syntactic discipline and show how it pro...

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
• Keywords: Alloy, Alloy Modeling Language, Alloy Specifications, FM 2009, Natural Language Processing