Synthesizing Contracts Correct Modulo a Test Generator

We present an approach that learns contracts for object-oriented programs where guarantees of correctness of the contracts are made with respect to a test generator. Our contract synthesis approach is based on a novel notion of tight contracts and an online learning algorithm (for tight contracts) that works in tandem with a test generator. We implement our approach and evaluate it on a suite of programs written in C#, studying the safety and strength of the synthesized contracts, and compare them to those synthesized by Daikon.

Presented at OOPSLA 2021, part of SPLASH 2021.
By Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, Tao Xie