SHF: Medium: Usable Property-Based Testing

Property-based testing (PBT) is a contemporary software engineering methodology in which users write executable formal specifications of system components and an automated test harness checks these specifications against many automatically generated inputs. PBT has become the testing method of choice across much of the functional programming community, and it is making inroads into industrial practice at companies such as Amazon, Volvo, Strip, Galois, and IOG. However, one thing remains a significant concern: A recent need-finding study of professional software developers who use PBT revealed great enthusiasm about the usefulness of PBT but frustration with its usability. This project’s impacts are accelerating the adoption of PBT by amplifying its power and solving key usability issues. To achieve these impacts, the project advances, in parallel, the tools developers use to write specifications, generate random inputs, and assess the strength of their test suites. The project’s novelties are the development of more configurable (“reflective”) generators, specification languages, and in-editor interfaces for visualizing and tuning distributions of generated inputs. In addition, this project launches new curricula for teaching mature and powerful PBT practices in the undergraduate and master’s classrooms. The project is developing novel techniques for PBT by bringing together methods from programming languages and human-computer interaction (HCI). First, it is working to establish an understanding of user needs with HCI studies of PBT in industry and real-time observations of developers interacting with PBT tools. Second, it is developing new abstractions for random input generation that enable a range of novel use cases—generating inputs satisfying validity conditions and tuning distributions based on examples or coverage—alongside benchmarks for evaluating PBT tools. Third, it is developing more usable specification tools, including a language for temporal properties over program traces and a programming assistant that helps programmers imagine and implement properties. And fourth, it is contributing new tools for effective interaction between developers on their tests, and in particular tools for visualizing and manipulating generated data distributions. The ultimate goal is to advance the state of the art in PBT and put it on every software developer’s toolbelt. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.