Function contracts are implemented using a goto-instrument pass that performs a whole program transformation.

Code Contracts Transformation Specification gives a specification of the transformation
Code Contracts Software Architecture describes the software architecture implementing the transformation