EvoSpex: A Search-Based Tool for Postcondition Inference

Postconditions are predicates that specify the intended behavior of a program by capturing properties about the program state when the program finishes its execution. Although postconditions can help to improve many software reliability analyses, they are seldom found accompanying source code. Thus, tools that assist developers in specifying postconditions are useful. This tool demo paper presents EvoSpex, a tool based on evolutionary computation that automatically infers postconditions of Java methods. Given a target Java method and a test suite for it, our tool executes the test suite to obtain valid pre/post state pairs for the method under analysis. Then, these pairs are mutated to obtain (allegedly) invalid ones, and finally a postcondition assertion characterizing the current method behavior is produced, by using an evolutionary algorithm that searches for an assertion that is satisfied by the valid pre/post state pairs and leaves out the invalid ones. EvoSpex implements a classic genetic algorithm that explores the space of candidate postconditions over a JML-like specification language. The algorithm is guided by a fitness function that aims at precisely capturing the valid state pairs, rejecting the invalid ones, and that also favors more succinct assertions. CCS CONCEPTS • Software and its engineering → Specification languages; Software verification and validation; Software testing and debugging.