Contract Soundness for Object-Oriented Languages

Abstract

Checking pre- and post-conditions of procedures and methods at runtime helps improve software reliability. In the procedural world, pre- and post-conditions have a straightforward interpretation. If a procedure's pre-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the procedure failed to compute the expected result.