Program Structure Aware Precondition Generation

TL;DR

This paper presents a new method for inferring natural, high-quality preconditions from code by leveraging program structure, improving readability and human reasoning, and scalable to large datasets of real-world Java projects.

Contribution

It introduces a structure-aware precondition inference technique that enhances readability and scalability, outperforming prior predicate-based methods.

Findings

Humans find preconditions inferred by our method easier to understand.

Our framework scales to large datasets, producing ~18k Java method-precondition pairs.

The approach improves the naturalness and correctness of inferred preconditions.

Abstract

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.