Program Structure Aware Precondition Generation

Fuente: arXiv
Gespeichert in:
Bibliographische Detailangaben
Hauptverfasser: Dinella, Elizabeth, Lahiri, Shuvendu, Naik, Mayur
Format: Preprint
Veröffentlicht: 2023
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1866909289595011072
author Dinella, Elizabeth
Lahiri, Shuvendu
Naik, Mayur
author_facet Dinella, Elizabeth
Lahiri, Shuvendu
Naik, Mayur
contents We introduce a novel approach for inferring natural preconditions from code. Our technique produces preconditions of high quality in terms of both correctness (modulo a test generator) and naturalness. Prior works generate preconditions from scratch through combinations of boolean predicates, but fall short in readability and ease of comprehension. Our innovation lies in, instead, leveraging the structure of a target method as a seed to infer a precondition through program transformations. Our evaluation shows that humans can more easily reason over preconditions inferred using our approach. Lastly, we instantiate our technique into a framework which can be applied at scale. We present a dataset of ~18k Java (method, precondition) pairs obtained by applying our framework to 87 real-world projects. We use this dataset to both evaluate our approach and draw useful insights for future research in precondition inference.
format Preprint
id arxiv_https___arxiv_org_abs_2310_02154
institution arXiv
publishDate 2023
record_format arxiv
spellingShingle Program Structure Aware Precondition Generation
Dinella, Elizabeth
Lahiri, Shuvendu
Naik, Mayur
Software Engineering
Programming Languages
We introduce a novel approach for inferring natural preconditions from code. Our technique produces preconditions of high quality in terms of both correctness (modulo a test generator) and naturalness. Prior works generate preconditions from scratch through combinations of boolean predicates, but fall short in readability and ease of comprehension. Our innovation lies in, instead, leveraging the structure of a target method as a seed to infer a precondition through program transformations. Our evaluation shows that humans can more easily reason over preconditions inferred using our approach. Lastly, we instantiate our technique into a framework which can be applied at scale. We present a dataset of ~18k Java (method, precondition) pairs obtained by applying our framework to 87 real-world projects. We use this dataset to both evaluate our approach and draw useful insights for future research in precondition inference.
title Program Structure Aware Precondition Generation
topic Software Engineering
Programming Languages
url https://arxiv.org/abs/2310.02154