Towards an Operational Semantics for Alloy

Download Now Free registration required

Executive Summary

The Alloy modeling language has a mathematically rigorous denotational semantics based on relational algebra. Alloy specifications often represent operations on a state, suggesting 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 the authors demonstrate the subtlety of representing state in Alloy specifications. They 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.

  • Format: PDF
  • Size: 155.8 KB