Alloy is one of few formal methods that enables its user to express rich structural properties of systems and mechanically check those properties for validity. It has been taught in at least nineteen universities around the world and serves as the foundation of a forthcoming book on software specification.
Alloy comprises three key elements: a logic, a language, and an analysis. The Alloy logic is a first-order logic with sets, relations, and transitive closure. The language is a simple and intuitive notation for expressing and structuring specifications in the logic. The analysis is embodied in the Alloy Analyzer, which mechanically checks properties expressed in the language for validity. The Analyzer performs an exhaustive search for a counterexample to a claimed property, within bounds that the user provides. If it finds a counterexample, the counterexample is guaranteed to represent a true violation of the property; however, the analysis can fail to find counterexamples when they require larger bounds for their detection. Nevertheless, in practice most counterexamples are found in small bounds.
Alloy is useful for modeling systems from a variety of domains. Unlike most formal methods, Alloy can easily express structural properties of systems. Such structural properties are crucial to expressing the correctness of linked data structures and data structure operations, which are pervasive in object-oriented software. Alloy is also conducive to modeling the behavior of abstract state machines, and users can apply the analysis to search for traces of state machines that violate a claimed property. The inherent non-determinism in Alloy allows distributed algorithms to be readily specified as well. The
Alloy Analyzer provides a wide array of visualization options, so regardless of the domain, simulations of systems and counterexamples to properties can be presented to the user in an intuitive way.
