PRECISE Seminar: Assertion-driven Development and Analyses

To increase reliability, developers have long used assertions -- logical statements that are expected to be true -- as lightweight specifications of crucial properties of code.  Assertions have predominantly served two purposes: documentation and runtime checking. We envision a far broader role of assertions where they are the cornerstone of a wide range of analyses that synergistically promise to bring about an unprecedented increase in reliability.

This talk describes our ongoing work on assertion-driven development and analyses, where developers first assert designs and then write code, static analyses check conformance of code to designs, testing checks correctness of executable code, and runtime checking detects erroneous executions, which error recovery repairs as desired.  Our vision is to enable new analyses that uniformly apply across the whole spectrum of software design, development, and maintenance -- static checking, testing, runtime checking, and error recovery all use the same assertions that developers write just once.  Consequently, writing assertions becomes much more attractive.  As developers write more assertions, they benefit not only from the new analyses but also from leveraging a host of existing analyses that utilize assertions.