Tool-Support Program Abstraction

Abstraction is a fundamental step in the construction of models for software systems. The abstraction techniques used in Bandera are based on abstraction-based program specialization (ABPS): a combination of abstract interpretation and partial evaluation technologies.

To construct an abstract model of a software system using ABPS, the model designer associates each program variable with an abstraction class. An abstraction class is an abstract version of a regular concrete Java class. The abstraction class abstracts away from various details of the original Java class and only retains information that is relevant for the particular software specification to be verified. For example, a stack class might be abstracted so that only information about the stack's size is retained (the actual contents are abstracted away).

Abstraction classes are defined using the Bandara Abstraction Specification Language (BASL). The BASL compiler translates a BASL specification to the Java implementation of the specified abstraction class. Compiled abstraction class are held in a library, allowing the model designer to easily reuse common abstractions.