The ABS Tool Suite

Syntax- and Type-Checking

To check an ABS model (a set of ABS files) for syntax and type-errors, run

java -jar absfrontend.jar <absfiles>

Java Code Generation and Execution

Java code generation is done by the ABS Java backend.

java -cp absfrontend abs.backend.java.JavaBackend -d <targetdir> <absfiles>

java -cp <targetdir>:absfrontend.jar <MainModule>.Main

Maude Code Generation and Execution

The Maude backend is responsible for generating Maude code from ABS models. Maude is a tool for executing models defined in rewriting logic.

java -cp absfrontend.jar abs.backend.maude.MaudeCompiler <absfiles> -o <outputfile>.maude

rew start .

Product Validation

Products are validated with respect to a given feature model using the ABS tools. For example, the following command verifies that the product HighEnd satisifies the feature model (both feature model and product are defined in the ChatPL.abs file).

java -cp absfrontend.jar abs.frontend.parser.Main -check=HighEnd ChatPL.abs

Flattening ABS models

Flattening an ABS model means applying a sequence of deltas to a core ABS model, in order to obtain the behaviour of a particular product. In the ABS compiler front end, the -product=name switch triggers the flattening for the given product. For example:

java -jar absfrontend.jar -product=P1 HelloWorld.abs

The flattening process is performed at the level of the AST, which is subsequently used to generate Java code.

Installation and usage instructions

COSTABS parameters

• Cost model: Briefly, a cost model is a function that maps each instruction to the amount of resources consumed when executing it. COSTABS provides the following cost models: termination, steps, memory, objects and task-level.
• Cost centers: Enabling this feature COSTABS will obtain the cost per component (also called cost-centers) rather than a single cost expression. The current implementation of COSTABS assumes that objects of the same type belong to the same cost center, i.e., they share the processor.
• Size norm: When a program manipulates numerical data, its cost often depends on the initial (integer) values of the corresponding variables. However, when it manipulates terms (i.e., data-structures), its cost usually depends on the sizes of the inputs. A size norm is a function that maps terms to numerical values that represent their sizes. The following size norms are available in COSTABS: term-size, which corresponds to the number of type constructors in a given term, and, term-depth, which corresponds to the length of the longest path in the term.
• Debugging mode: The debugging mode produces on-screen detailed information of the different phases and generates files with some useful intermediate information such as the rule-based representation (an intermediate representation for ABS programs) and the cost-relation system.
• Asymptotic bounds: Enabling this feature COSTABS obtains asymptotic upper-bounds rather than concrete upper-bounds.
• Verbosity: COSTABS allows setting three verbosity levels, named 0 (the least verbose) to 2 (the most verbose).

For more details on the meaning of the COSTABS parameters go to chapter 3 of deliverable 4.2.

Helping the analyzer with class invariants

COSTABS provides a way to incorporate class invariants on the analyzed ABS code. Those invariants can provide, e.g., guarantees on the global states when the process is resumed after an await statement. Annotations can be written right before await statements or right before method definitions (currently those are the only places where they can be needed). The are written in ABS format, each annotation between []’s, with the special functions ‘old’, ‘max’ and ‘min’. See the annotations in the ABS examples at the COSTABS web site.

For example, if we add the following invariant

[old(f) == f][f <= max(f)][f > 0]

right before an await instruction then we state that it is guaranteed that when the process resumes, the value of field f will be the same as when the process was suspended, and also that f is bounded by var max(f) and it is always positive. This kind of invariants are sometimes needed in order for the analyzer to bound the number of iterations on loops.

See more details on chapter 3 of deliverable 4.2

Note: In the previous version of COSTABS invariants were written in a pseudo-JML format. E.g., the one above was written

//@invariant \old(f) == f

This syntax is not valid anymore since we are now adhering to the ABS annotations format.