DynAlloy is an extension of the formal specification language Alloy. Alloy is a relatively popular formal specification language because of various reasons, including:
it has simple formal semantics, based on relations
its syntax is simple, with a few constructs (with intuitive meaning)
its specifications follow an OO-like style
it is designed with fully automated analysis support in mind
Alloy is a model-oriented specification language, similar to other formal languages such as Z, VDM and B. As for these other languages, specifications (or models, as these are more often called) are written by defining data domains, properties and operations between these domains. This tutorial assumes that the reader is familiar with Alloy; we refer the reader to the Alloy Online Tutorial for more information, examples, etc., regarding Alloy.
Alloy is suitable for specifying static structural properties of systems, but is less adequate for the specification of dynamic properties of systems, i.e., properties regarding executions. DynAlloy extends Alloy by incorporating the notion of action to better describe state change and properties of state changing situations.