Falling Back on Executable Specifications

European Conference on Object-Oriented Programming (ECOOP 2010), Maribor, Slovenia, June 21-25, 2010.
Hesam Samimi, Ei Darli Aung, Todd Millstein
We describe a new approach to employing specifications for software reliability. Rather than only using specifications to validate implementations, we additionally employ specifications as a reliable alternative to those implementations. Our approach, which we call Plan B, performs dynamic contract checking of methods. However, instead of halting the program upon a contract violation, we employ a constraint solver to automatically execute the specification in order to allow the program to continue properly. This paper describes Plan B as well as its instantiation in an extension to Java with executable specifications that we call PBnJ (Plan B in Java). We present the design of PBnJ by example and describe its implementation, which leverages the Kodkod relational constraint solver. We also describe our experience using the language to enhance the reliability and functionality of several existing Java applications.

[PDF | Implementation | Project Page]