Inferring Natural Preconditions via Program Transformation
Elizabeth Dinella, Shuvendu K. Lahiri, Mayur Naik · 2024
We introduce an approach for inferring natural preconditions from code. Prior works generate preconditions from scratch through combinations of boolean predicates, but fall short in readability and ease of comprehension. In contrast, our technique leverages the structure of the target method as a seed to infer a precondition through program transformations. Our technique is a multi-phase approach involving iterative test generation and program transformation. Our evaluation shows that humans can more easily reason over preconditions inferred using our approach. Consumers of our preconditions completed reasoning tasks more accurately (92.86%) with an average total duration of 109 seconds. In contrast, consumers of the preconditions inferred by prior work took twice as long (217 seconds) to finish the study and answered with lower accuracy (85.61%).