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]