EvoSpex is a search-based tool for inferring postconditions of Java methods. Given a Java method and a test suite with executions of the method, EvoSpex uses evolutionary computation to automatically infer a postcondition assertion capturing the method's current behavior. EvoSpex relies on a state generation technique to generate program states caracterizing current behavior as well as potentially invalid behavior, and then produces an assertion distinguishing between these program states. The assertions that EvoSpex produce belong to a JML-like specification language. Contributions to this repo are welcome!
Check out our demo video!
- Apache Maven (tested with version 3.8.5)
- Java >= 8
To build and install EvoSpex locally, clone this repository and run the following command:
mvn clean compile assembly:single
mvn test-compileComing soon!
Given a Java class containing the target method and a test suite with execution of the method, the use of EvoSpex requires two phases. A state generation phase and an inference phase. The state generation phase generates valid states characterizing the current behavior of the target method and invalid states representing invalid behavior of the target method.
To perform the state generation phase, run the following command:
./evospex.sh --genStates <cp> <test_suite> "<method>"where <cp> is the target subject classpath, <test_suite> is the target test suite fully quallified name and "<method>" is the target method signature. This phase will produce, in the states folder, the files containing the states for the current target method.
After generating the states, to perform the inference phase and generate the postcondition assertion, run the following command:
./evospex.sh --infer <cp> <class> <method_states>where <method_states> is the folder containing the states produced in the previous phase. The execution will report information of each generation of the evolutionary process (mutations performed, crossovers performed, best fitness value, etc). At the end, the candidate postcondition is reported in the form of an assertion.
As an example, let us consider method add(int, java.lang.Object) of class TreeList, took from the Apache Commons Collections repository. This method inserts an element in a specific position on an avl-tree based implementation of lists. To generate a postcondition assertion for this method, and using as input the test suite TreeListRegressionTest0, automatically generated with Randoop the two phases can be performed as follows:
./evospex.sh --genStates target/test-classes/ casestudies.commonscollections.TreeListRegressionTest0 "<casestudies.commonscollections.TreeList: void add(int,java.lang.Object)>"
./evospex.sh --infer target/evospex.jar casestudies.commonscollections.TreeList states/casestudies.commonscollections.TreeList/_void_add\(int,java.lang.Object\)/EvoSpex reports the postcondition as an assert statement: assert(...);. For instance, for the above example, an execution of EvoSpex may return a postcondition such as the following:
assert(
this.size = \old(this.size) + 1 &&
#(old(this).root.*(left+right))=this.size-1 &&
index in this.root.*(left).height &&
obj in this.root.*(left+right).value
);| Parameter | Description | Example | Default value |
|---|---|---|---|
| popSize | Evolutionary algorithm population size | popSize=1000 | 500 |
| gens | Evolutionary algorithm generations | gens=500 | 100 |
| to | Evolutionary algorithm timeout (in seconds) | to=1800 | 600 |
| mp | Mutation probability | mp=0.2 | 0.3 |
| cp | Crossover probability | cp=0.6 | 0.55 |
The evaluation subjects can be found here:
To run EvoSpex on all the subjects you can follow the instructions in this page.
If you experience any issues, please submit an issue or contact us at [email protected]!