Leon Gendler 
DISCERN: Towards the Automatic Discovery of Software Contracts

Design by contract is a practical methodology for evolving code together
with its specification. The contract is expressed as a set of class
invariants and method pre- and postconditions. These assertions have
important methodological implications on the client-supplier and
inheritance relationships between classes. In addition, tools that
instrument the code to check for contract violations help development by
catching errors close to their sources.

Unfortunately, writing (and maintaining) contracts requires a
non-trivial investment of time and effort. We are developing a tool,
called DISCERN, to statically analyze existing programs and discover
draft contracts for them. DISCERN works by propagating weakest
preconditions and strongest postconditions through the code. Known pre-
and postconditions of operations used in the code help refine the
contract; conversely, new assertions discovered can be propagated to
clients of the method being analyzed. As usual, loops make the analysis
difficult; heuristics are used to recognize the most common loop forms
and extract useful information about them.

This talk reports on our results using weakest precondition propagation
to discover method preconditions and candidates for class invariants. We
have used DISCERN on classes from the Java libraries, and have
successfully identified preconditions and invariants that are required
for correct use of these libraries.