Alloy
Wikipedia on Answers.com:
Top
Alloy (specification language)
In computer science and software engineering, Alloy is a declarative specification language for expressing complex structural constraints and behavior in a software system. Alloy provides a simple structural modeling tool based on first-order logic. The mathematical underpinnings of the language were heavily influenced by the Z notation, although the syntax of Alloy owes more to languages such as Object Constraint Language.[1] Alloy is targeted at the creation of micro-models that can then be automatically checked for correctness. Alloy specifications can be checked using the Alloy Analyzer.
The first version of the Alloy language appeared in 1997. It was a rather limited object modeling language. Succeeding iterations of the language "added quantifiers, higher arity relations, polymorphism, subtyping, and signatures".[2] Although Alloy is designed with automatic analysis in mind, Alloy differs from many specification languages designed for model-checking in that it permits the definition of infinite models. The Alloy Analyzer is designed to perform finite scope checks even on infinite models.
Model structure
 |
This unreferenced section requires citations to ensure verifiability. |
Alloy models are relational in nature, and are composed of several different kinds of statements:
- Signatures define the vocabulary of a model by creating new sets
-
sig Object{}defines a signature Objectsig List{ head : lone Node }defines a signature List that contains a field head of type Node and multiplicity lone - this establishes the existence of a relation between Lists and Nodes such that every List is associated with no more than one head Node
- Facts are constraints that are assumed to always hold
- Predicates are parameterized constraints, and can be used to represent operations
- Functions are expressions that return results
- Assertions are assumptions about the model that can be checked using the Alloy Analyzer
Because Alloy is a declarative language the meaning of a model is unaffected by the order of statements.
References
- ^ Jackson, Daniel (2006). Software Abstractions: Logic, Language, and Analysis. MIT Press. ISBN 978-0-262-10114-1.
- ^ "Alloy FAQ". http://alloy.mit.edu/faq.php. Retrieved 2007-05-16.
External links
 |
This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)
Post a question - any question - to the WikiAnswers community:
Copyrights:
Wikipedia on Answers.com
This article is licensed under the Creative Commons Attribution/Share-Alike License. It uses material from the Wikipedia article Alloy (specification language).
Read more