The Bandera abstraction components provide automated support for
reducing model size via data abstraction. This is useful when a
specification 
to be checked does not depend on the program's
concrete values but instead depends only on properties of those
values. For example, an application might store a set of items in a
vector, but if the property being verified depends only on whether a
particular item is in the vector, we could abstract the large number
of vector states onto a small set
.
The user guides the abstraction process by binding variables to entries from an abstraction library. The library entries are indexed by concrete type, and each entry implements an abstract version of its corresponding concrete type. Each abstraction in the library is defined using the Bandera Abstraction Specification Language (BASL). A BASL specification for a base type abstraction consists of a declaration of a finite set of abstract tokens, an abstraction function that maps each concrete Java value to an abstract token, and an abstract operation for each operation of the concrete type. A rule-based format that incorporates pattern matching simplifies the definition of abstract operations. For base type abstractions, the BASL compiler allows the user to supply an abbreviated BASL specification containing only the abstract token set and abstraction function. It then uses the PVS theorem prover to automatically synthesize the abstract versions of operations such as +, -, etc. This makes it extremely easy to define new abstractions on base types. Given a (possibly synthesized) BASL specification, the BASL compiler generates a Java class containing methods that implement the defined abstraction function as well as abstract versions of the relevant concrete operators. The Java class is held in the library, and is linked with rest of source code during model-generation if the user has selected that particular abstraction.
Since abstractions are incorporated on a per variable basis, two
different variables of the same concrete type can have different
abstract types. For example, if 
and 
are both int
abstractions, then variable int x may be bound to and
variable int y may be bound to . After the user has chosen
abstractions for a few key variables that are relevant to the property
being checked, a type inference phase propagates this information
throught the program and infers abstraction types for the remaining
variables and for each expression in the program. Type inference also
informs the user when there is an abstraction type error.
Once abstract type inference is run, the abstraction engine will
transform the source code into a specialized version where all
concrete operations and tests on the relevant objects (e.g., method
calls on the vector class) are replaced with abstract versions that
manipulate tokens representing the abstract values
. Since
information is lost in this transformation, operations and tests that
relied on the lost information can no longer be determined completely
in the abstract program. For instance, in the vector example the
length of the abstracted vector cannot be determined. Any conditional
test that consulted the vector's length would be transformed into a
non-deterministic choice between the true and false branches.
As with slicing, the abstracted code is represented at the
Jimple level, but JJJC can decompile it back to Java.