Executable assertions and separate compilation

The use of executable assertions is widely recognised as a useful programming technique for complex systems. In many cases static analysis of programs allows such assertions to be removed at compile time, thus removing the overhead of the test. The use of interprocedural analysis would often allow a larger number of such tests to be statically removed; intermodular analysis could even improve overall safety of the system. In general, however, such analysis is antithetical to separate compilation and extensible systems. In this paper we offer a partial solution to this dilemma: We propose that preconditions become part of the interface definition of an encapsulated object. The implementation consequences of this technique are explored.