Design and implementation of assertions for the Common Language Infrastructure

Assertions are a well established mechanism for the specification and verification of program semantics in the forms of preconditions, post-conditions and invariants of object and component interfaces. Traditionally, assertions are typically specific to individual programming languages. The ECMA Common Language Infrastructure (CLI) provides a shared dynamic execution environment for implementation and interoperation of multiple languages. The authors extend the CLI with support for assertions, in the design by contract style, in a language-agnostic manner. Their design is flexible and powerful in that it treats assertions as first class constructs in both the binary format and in the run-time while leaving the source level specification choices completely open. The design also enforces behavioural sub-typing and object re-entrance rules, and provides sensible exception handling. The implementation of run-time monitoring in Microsoftʹs Shared Source CLI (a.k.a. Rotor) integrates with the dynamic runtime, performing just-in-time code weaving in a novel way to maximise efficiency while operating at the platform-neutral level.