Microsoft Code Contracts

Microsoft Code Contracts is a .NET library introduced by Microsoft that allows developers to specify rules (contracts) in code to formally describe how methods and classes should behave.

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.

Code Contracts bring the advantages of design-by-contract programming to all .NET programming languages.

What is a Code Contract?

Think of Code Contracts as “rules written inside your code”.

Instead of only writing logic, you also write:

• “This value must not be null”
• “This number must be positive”
• “This method always returns a non-empty list”

Then the system checks these rules at:

• Compile time (static analysis)
• Runtime (if enabled)

Why Code Contracts exist?

Traditional C# checks:

• If something breaks → runtime exception

Code Contracts:

• Detect issues before runtime
• Improve code correctness and documentation
• Reduce bugs in complex systems

Key concepts about Code Contracts

1. Preconditions

What must be true before a method runs.

Contract.Requires(x > 0);

Meaning: “x must be greater than 0 or stop execution.”

2. Postconditions

What must be true after a method finishes.

Contract.Ensures(Contract.Result() > 0);

Meaning: “this method always returns a positive number.”

3. Object invariants

Conditions that must always remain true for a class.

Contract.Invariant(balance >= 0);

Meaning: “balance can never be negative.”

4. Assumptions

Tell the analyzer to assume something is true.

Contract.Assume(list != null);

Why use Code Contracts?

1. Early bug detection

Find issues before running the program.

2. Better documentation

Contracts describe intent more clearly than comments.

3. Safer refactoring

Compiler and analyzer help ensure correctness.

4. Formal verification

Some checks can be mathematically analyzed.

When should you use it?

Code Contracts are useful when:

• You work on large, complex systems
• You need high reliability (finance, aerospace, etc.)
• You want strict API correctness
• You maintain legacy enterprise code

Less useful when:

• Building small apps or prototypes
• Using modern lightweight validation approaches

Advantages

• Catches bugs early
• Improves code clarity
• Reduces defensive programming
• Helps enforce API rules

Disadvantages

• Adds extra complexity
• Static analysis can be slow or incomplete
• Limited modern support (project is effectively deprecated)
• Not widely adopted today
• Requires learning new patterns

Alternatives in modern .NET

1. Built-in nullable reference types

• string name = null; // warning

2. Guard clauses

• if (b == 0) throw new ArgumentException();

3. FluentValidation

• External validation library for business rules.

4. Static analyzers

• Roslyn analyzers
• ReSharper inspections

The benefits of code contracts

• Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

• Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.

• Static verification: The static checker can decide whether there are any contract violations without running the program. It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

• Reference documentation: The documentation generator augments existing XML documentation files with contract information. There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

Why to use Code Contracts?

Object-oriented languages already include contracts; “classic” signature-checking involves verification of parameter counts and type-conformance. Design-by-contract (DBC) generally means extending this mechanism to include assertions on a higher semantic level. A method’s signature describes the obligations calling code must fulfill in order to execute the method. The degree of enforcement varies from language to language. Statically-typed languages verify types according to conformance at compile-time, whereas dynamically-typed languages do so at run-time. Even the level of conformance-checking differs from language to language, with statically-typed languages requiring hierarchical conformance via ancestors and dynamically-typed languages verifying signatures via duck-typing.

And that’s only for individual methods; methods are typically collected into classes that also have a semantic meaning. DBC is about being able to specify the semantics of a class (e.g. can property A ever be false when property B is true?) as well as those of method parameters (can parameter a ever be null?) using the same programming language.