No.050 Software Contracts for Communication, Monitoring, and Security

A major obstacle facing adoption of formal software verification is the difficulty to track changes in the target code and to accomodate them in specifications and in verification arguments. We introduce fully abstract method contracts, a new verification rule for method calls that can be used in most contract-based verification settings. The rule makes it possible to reason about programs without having to know the implementation of called methods. By combining abstract method contracts and caching of verification conditions, it is possible to detect reusability of contracts automatically via first-order reasoning. This is the basis for a verification framework able to deal with code undergoing frequent changes. Fully abstract contracts have been implemented in the Java verification tool KeY. We report on experiments that show their saving potential.

The standard algorithm for higher-order contract checking

can lead to unbounded space consumption and can destroy tail
recursion. In this work, we show how to achieve space efficiency for
contract checking. Working in a manifest context, we define a family
of languages: classic λH, which is inefficient; forgetful λH, which is
efficient but skips some checks; and heedful λH, which is efficient
but may change blame labels. We show first that if classic λH produces
a value, then so does forgetful λH (but not vice versa); we then show
that classic and heedful λH yield identical values, but possibly
differing blame labels.