|
A small strongly typed language built upon rigorous semantics
and ideas from the Z specification language
[Home Page,
Definition].
The question posed by the author:
"What is the smallest modelling notation that can express
a useful range of structural properties, is
easy to read and write, and can be analyzed automatically?"
Alloy supports the description of basic structure
(graphically, or as textual declarations),
as well as more intricate constraints and operations
describing how structures change dynamically
(both expressed as logical formulas)...
Alloy is not for describing dynamic interactions between objects,
nor for describing syntactic structure in an implementation,
such as the class hierarchy and packaging...
Alloy is amenable to a fully automatic semantic analysis
that can provide checking of consequences and consistency,
and simulated execution.
To gain ‘executability’, Alloy does not sacrifice abstraction:
it can generate sample transitions of an operation
described implicitly, using negation and conjunction."
A file system is used as an example. A comparison is made to UML and UML's Object Constraint Language. A critique of how Z's reliance on Latex has limited its widespread use is also given. See the Authors Home Page for software download, talks, publications, and access to a Yahoo discussion group.
Posted to OOP by jon fernquest on 8/12/02; 2:05:58 AM
|
|
Alloy: A Lightweight Object Modelling Notation
