The Binary Rewriter

The Intermediate Language (IL) that the C# compiler produces for the above example cannot be executed as is. To provide for the runtime checking of contracts, the binary rewriter takes the compiled IL and transforms it so that contracts are evaluated at the correct program points. For instance, postconditions are evaluated just before each return point within a method. Any expression within a call to OldValue() is evaluated upon entry into the method with the corresponding value replacing the call when the postcondition is evaluated. (There is also the method Result() which is used to refer to the return value of a method. Its use is illustrated below.) If the instrumented code happens to follow an execution path that violates a contract, then there is a programmable notification component that signals an error. You can see an example in the screenshot below, which shows a precondition that failed at runtime: the method Divide was expecting a non-zero argument. (For this example, the notification resulted in an assert dialog, but you can customize it to perform any action you would like.)