*Powered by*

## A Case for Alloy Annotations for Efficient Incremental Analysis via Domain Specific Solvers

Svetoslav Ganov, Dewayne Perry, and Sarfraz Khurshid

*(University of Texas at Austin, USA)*

Abstractâ€”Alloy is a declarative modelling language based
on first-order logic with sets and relations. Alloy formulas are
checked for satisfiability by the fully automatic Alloy Analyzer.
The analyzer, given an Alloy formula and a scope, i.e. a bound on
the universe of discourse, searches for an instance i.e. a valuation
to the sets and relations in the formula, such that it evaluates to
true. The analyzer translates the Alloy problem to a propositional
formula for which it searches a satisfying assignment via an off-
the-shelf propositional satisfiability (SAT) solver. The SAT solver
performs an exhaustive search and increasing the scope leads to
the combinatorial explosion problem.
We envision annotations, a meta-data facility used in impera-
tive languages, as a means of augmenting Alloy models to enable
more efficient analysis by specifying the priority, i.e. order of
solving, of a given constraint and the slover to be used. This
additional information would enable using the solutions to a
particular constraint as partial solutions to the next in case
constraint priority is specified and using a specific solver for
reasoning about a given constraint in case a constraint solver is
specified.

**» Back to Papers**