EvoSpex: An Evolutionary Algorithm for Learning Postconditions
Software reliability is a primary concern in the construction of software, and thus a fundamental component in the definition of software quality. Analyzing software reliability requires a specification of the intended behavior of the software under analysis, and at the source code level, such speci...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Objeto de conferencia Resumen |
| Lenguaje: | Inglés |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/140422 http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-07.pdf |
| Aporte de: |
| id |
I19-R120-10915-140422 |
|---|---|
| record_format |
dspace |
| institution |
Universidad Nacional de La Plata |
| institution_str |
I-19 |
| repository_str |
R-120 |
| collection |
SEDICI (UNLP) |
| language |
Inglés |
| topic |
Ciencias Informáticas Java Tools Genetics Software reliability Genetic algorithms Contracts Software engineering |
| spellingShingle |
Ciencias Informáticas Java Tools Genetics Software reliability Genetic algorithms Contracts Software engineering Molina, Facundo Ponzio, Pablo Daniel Aguirre, Nazareno Matías Frias, Marcelo F. EvoSpex: An Evolutionary Algorithm for Learning Postconditions |
| topic_facet |
Ciencias Informáticas Java Tools Genetics Software reliability Genetic algorithms Contracts Software engineering |
| description |
Software reliability is a primary concern in the construction of software, and thus a fundamental component in the definition of software quality. Analyzing software reliability requires a specification of the intended behavior of the software under analysis, and at the source code level, such specifications typically take the form of assertions. Unfortunately, software many times lacks such specifications, or only provides them for scenario-specific behaviors, as assertions accompanying tests. This issue seriously diminishes the analyzability of software with respect to its reliability, emphasizing the well known Oracle Problem.
We tackle this problem by proposing a technique that, given a Java method, automatically produces a postcondition assertion of the method's current behavior. This mechanism is based on generating valid and invalid pre/post state pairs (i.e., state pairs that represent, and do not represent, the method's current behavior, respectively), which guide EvoSpex, a genetic algorithm, to produce a JML-like assertion characterizing the valid pre/post pairs, while leaving out the invalid ones. The generation of valid pre/post pairs is based on executing the method on a bounded exhaustive test set, generated by exercising the method inputs' APIs. The invalid pairs, on the other hand, are obtained by mutating valid pairs modifying the post-states so that each resulting pair does not belong to the set of valid pairs. EvoSpex searchs for an adequate postcondition assertion expressed in a JML-like language that involves quantification, object navigation and reachability expressions, making our approach particularly well-suited for reference-based class implementations with (implicit) strong representation invariants, such as heap-allocated structural objects, and complex custom types.
We evaluated our technique on a benchmark of open source Java projects, featuring complex implementations of reference-based classes. In these case studies, EvoSpex was able to generate post-conditions that were stronger and more accurate, than those generated by related specification-inference approaches, as evaluated by an automated oracle assessment tool. Moreover, EvoSpex was also able to infer an important part of manually written rich postconditions (strong contracts used for verification) present in verified classes, and reproduce contracts for methods whose class implementations were automatically synthesized from specifications. |
| format |
Objeto de conferencia Resumen |
| author |
Molina, Facundo Ponzio, Pablo Daniel Aguirre, Nazareno Matías Frias, Marcelo F. |
| author_facet |
Molina, Facundo Ponzio, Pablo Daniel Aguirre, Nazareno Matías Frias, Marcelo F. |
| author_sort |
Molina, Facundo |
| title |
EvoSpex: An Evolutionary Algorithm for Learning Postconditions |
| title_short |
EvoSpex: An Evolutionary Algorithm for Learning Postconditions |
| title_full |
EvoSpex: An Evolutionary Algorithm for Learning Postconditions |
| title_fullStr |
EvoSpex: An Evolutionary Algorithm for Learning Postconditions |
| title_full_unstemmed |
EvoSpex: An Evolutionary Algorithm for Learning Postconditions |
| title_sort |
evospex: an evolutionary algorithm for learning postconditions |
| publishDate |
2021 |
| url |
http://sedici.unlp.edu.ar/handle/10915/140422 http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-07.pdf |
| work_keys_str_mv |
AT molinafacundo evospexanevolutionaryalgorithmforlearningpostconditions AT ponziopablodaniel evospexanevolutionaryalgorithmforlearningpostconditions AT aguirrenazarenomatias evospexanevolutionaryalgorithmforlearningpostconditions AT friasmarcelof evospexanevolutionaryalgorithmforlearningpostconditions |
| bdutipo_str |
Repositorios |
| _version_ |
1764820458810638337 |