An Imperative Extension to Alloy

We extend the Alloy language with the standard imperative constructs; we show the mix of declarative and imperative constructs to be useful in modeling dynamic systems. We present a translation from our extended language to the existing first-order logic of the Alloy Analyzer, allowing for efficient analysis of models.

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Joseph P. Near, Daniel Jackson
• Keywords: Alloy Language, ASM 2010, Imperative Constructs, Microbiology, Standard Imperative Constructs