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.

翻译：我们提出了一种从代码中推断自然预条件的新方法。我们的技术能够在正确性（基于测试生成器验证）和自然性两个维度上生成高质量的预条件。现有工作通过布尔谓词组合从零开始生成预条件，但在可读性和易理解性方面存在不足。我们的创新在于利用目标方法的结构作为"种子"，通过程序变换来推断预条件。实验评估表明，人类能更容易地理解基于我们方法推断出的预条件。最后，我们将该技术实例化成一个可规模化应用的框架，并提供了通过该框架对87个真实项目处理得到的约1.8万个Java（方法，预条件）数据对。我们利用该数据集既评估了方法有效性，也为预条件推理领域的未来研究提供了有益启示。