Details

Our idea was to help guarantee the correct behavior when integrating an annotated component into a new system reusing it, creating a tool to automate this process. This integration should be smooth, in the sense of that it should not turn a correct system into an incorrect one.

To achieve this verification goal, it is necessary:

• to verify the component correctness with respect to its contract (using a traditional Verification Condition Generator, already incorporated in GamaSlicer, available at http://gamaepl.di.uminho.pt/gamaslicer);
• to verify if the actual calling context preserves the precondition;
• to verify if the component is properly used in the actual context after the call;
• Given a reusable component and a set of calling points, specify the component body according to the concrete calling needs.

The whole process is a bit complex and was divided in a set of smaller problems (divide and conquer). The tool under discussion focus on the second item, working with preconditions and backward slicing.

Figure 1 shows GamaPolarSlicer architecture, aiming at the easiness of the described process. The architecture is based on the classical structure of a language processor.

Source Code can be a Java project or only Java files to analyze by the tool.

Lexical Analyzer, Syntactic Analyzer, Semantic Analyzer the Lexical layer converts the input into symbols that will be later used in the Identifier Table. The Syntactic layer uses the result of the Lexical layer above and analyzes it to identify the syntactic structure of it. The Semantic layer adds the semantic information to the result returned by the Syntactic layer. It is in this layer that the identifier table is built. These three layers, usually are always present in language processors.

Invocations Repository is the data structure where all function calls processed during the code analysis are stored. The contract verification will be applied to each one of these calls and the slicing criterion of each one will consider the parameters struct.

Annotated Components Repository is the data structure where all components with a formal specification (precondition and postcondition at least) are stored. All these components will be later used in the slicing process in order to filter all the calls (from the invocation repository) defined without any type of annotation. This repository has an important role when verifying if the call respects the component contract.

Identifier Table flags, always, an important role on the implementation of the processor. All symbols and associated semantic processed during the code analysis phase are stored here. It will be one of the backbones of all structures and of all stages of the tool process.

Annotated System Dependency Graph is the internal representation chosen to support our slicing-based code analysis approach. Constructed during the code analysis, this type of graph allows to associate formal annotations, like preconditions, postconditions or even invariants, to the its nodes.

Caller-based Slicer is the layer where the backward slicing is applied to each annotated component call. It uses both invocations repository and annotated components repository to extract the parameters to execute the slicing for each invoked annotated component. The resulting slice is a Annotated System Dependency Graph, this a subgraph of the original Annotated System Dependency Graph, with all the statements relevant to the particular call.

Contract Verifier using the slice that resulted from the layer above, and using the component contract, this layer analyzes every node on the slice and verifies in all of them if there are guarantees that every annotation in the contract is respected.

Output Report describes all contract violations found during the whole process. All violations found are marked with the degree of relevance in order to aid the user in the revision process. In the future, the tool will allow the possibility to provide some suggestions to solve these issues, and a graphic display of the violations over the Annotated System Dependency Graph.