Towards an Operational Semantics for Alloy Export

@incollection{citeulike:6082904, 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 state-transition 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 provides a foundation for program synthesis from Alloy.}, author = {Giannakopoulos, Theophilos and Dougherty, Daniel and Fisler, Kathi and Krishnamurthi, Shriram}, citeulike-article-id = {6082904}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-05089-3_31}, citeulike-linkout-1 = {http://www.springerlink.com/content/h658l77147707554}, doi = {10.1007/978-3-642-05089-3_31}, journal = {FM 2009: Formal Methods}, keywords = {2009, alloy, operational\_semantics, semantics}, pages = {483--498}, posted-at = {2009-11-07 13:22:13}, priority = {4}, title = {Towards an Operational Semantics for Alloy}, url = {http://dx.doi.org/10.1007/978-3-642-05089-3_31}, year = {2009} }

TY - CHAP ID - citeulike:6082904 L3 - citeulike-article-id:6082904 N2 - 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 state-transition 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 provides a foundation for program synthesis from Alloy. JF - FM 2009: Formal Methods EP - 498 TI - Towards an Operational Semantics for Alloy SP - 483 KW - 2009 KW - alloy KW - operational_semantics KW - semantics AU - Giannakopoulos, Theophilos AU - Dougherty, Daniel AU - Fisler, Kathi AU - Krishnamurthi, Shriram PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-05089-3_31 ER -