Contracts are formal and verifiable specifications that extend traditional type definitions by including preconditions, postconditions, invariants, acceptable inputs and outputs, and other behavioral specifications [1]. These class-level specifications can be used to verify both usage and behavior of software components at runtime. This paper details the concept of blame, which is implemented in the Racket language. When a contract violation occurs, blame enables the system to accurately indicate the guilty party in the failed transaction.

First-class classes, or classes that are in themselves objects, enable new ways of composing class types without resorting to multiple inheritance. Some mainstream languages such as Java and C# do not support first-class classes, while Ruby and Python do. Contract systems are intended to specify conditions about values, and not about classes themselves, and their relationships. Contracts are specified at a class level. Contract systems do not normally support meta-definition of contracts or the sharing of contracts between different classes without duplication of code.

The authors present details of an innovative contract-based approach for working with first-class classes. The proposed approach includes both the design and implementation of a contract system for first-class classes, including some theoretical foundations and a formal proof of a new “blame correctness” theorem. The paper includes a practical evaluation and validation of the approach. It is well-researched and thorough, but its value is limited by a focus on both design by contract and languages that support first-class classes. However, the paper should prove valuable to those with interests in these areas.