Abstract Alloy Instances.

Alloy is a textual modeling language for structures and behaviors of software designs. One of the reasons for Alloy to become a popular light-weight formal method is its support for automated, bounded analyses, which is provided through the Analyzer toolset. The Analyzer provides the means to compute, visualize, and browse instances that either satisfy a model or violate an assertion. Understanding instances for the given analysis often requires much effort and there is no guarantee on the order or level of information of computed instances. To help address this, we introduce the concept of abstract Alloy instances, which abstract information common to all instances, while preserving information specific to the analysis. Our abstraction is based on introducing lower and upper bounds for elements that may appear in Alloy's instances. We evaluate computation times and sizes of abstract instances on a set of benchmark Alloy models.