Approach To Analysis
The Alloy Analyzer was specifically developed to support so-called "lightweight formal methods". As such, it is intended to provide fully automated analysis, in contrast to the interactive theorem proving techniques commonly used with specification languages similar to Alloy. Development of the Analyzer was originally inspired by the automated analysis provided by model checkers. However, model-checking is ill-suited to the kind of models that are typically developed in Alloy, and as a result the core of the Analyzer was eventually implemented as a model-finder built atop a boolean SAT solver.
Through version 3.0, the Alloy Analyzer incorporated an integral SAT-based model-finder based on an off-the-shelf SAT-solver. However, as of version 4.0 the Analyzer makes use of the Kodkod model-finder, for which the Analyzer acts as a front-end. Both model-finders essentially translate a model expressed in relational logic into a corresponding boolean logic formula, and then invoke an off-the-shelf SAT-solver on the boolean formula. In the event that the solver finds a solution, the result is translated back into a corresponding binding of constants to variables in the relational logic model.
In order to ensure the model-finding problem is decidable, the Alloy Analyzer performs model-finding over restricted scopes consisting of a user-defined finite number of objects. This has the effect of limiting the generality of the results produced by the Analyzer. However, the designers of the Alloy Analyzer justify the decision to work within limited scopes through an appeal to the small scope hypothesis: that a high proportion of bugs can be found by testing a program for all test inputs within some small scope.
Read more about this topic: Alloy Analyzer
Famous quotes containing the words approach to, approach and/or analysis:
“F.R. Leavis’s “eat up your broccoli” approach to fiction emphasises this junkfood/wholefood dichotomy. If reading a novel—for the eighteenth century reader, the most frivolous of diversions—did not, by the middle of the twentieth century, make you a better person in some way, then you might as well flush the offending volume down the toilet, which was by far the best place for the undigested excreta of dubious nourishment.”
—Angela Carter (1940–1992)
“I approach these questions unwillingly, as it wounds, but no cure can be effected without touching upon and handling them.”
—Titus Livius (Livy)
“Cubism had been an analysis of the object and an attempt to put it before us in its totality; both as analysis and as synthesis, it was a criticism of appearance. Surrealism transmuted the object, and suddenly a canvas became an apparition: a new figuration, a real transfiguration.”
—Octavio Paz (b. 1914)