How does "Contract.Requires<T>" behave without ccrewrite? Does this differ from "Requires"?

Question

When not using ccrewrite (say the project is built by another developer without CC installed),

Is Contract.Requires<T>(cond) silently stripped or does it still result in behavior equivalent to if (!cond) { throw new T() }? (I don't care if it's another method call or two - but it should "always be checked".)

I ask because Contract.Requires<T> appears to behave differently than Contract.Requires, but I'm not sure "how" or "when".

The goal is to replace the construct on public contracts

if (x != null) throw new ArgumentNullException();

with a CC-compatible version that will still throw an exception when not performing a CC rewrite during the build step.

While the above with EndContractBlock does work with "Custom Parameter Validation" (ie. legacy contract mode) I would like to use "Standard Contract Requires" in the project.

I believe there may be an equivalency, because in "Custom Parameter Validation" mode I am not able to use Requires<T>; if there is no equivalency to an always-required-check, insight as to why would be nice.

I am fine losing Requires, Ensures, and leaving in the non-honored invariant contract methods and interface contracts when CC rewriting is not done as I value them for the static analysis - but I need these always-there boundary checks to argue for keeping CC.

Answer 1

Please see the Code Contracts manual. It definitely tells you all you need to know about how the various forms of Code Contract checking works and what options are required to be set when using each form.

What's the Difference Between Contract.Requires(bool cond) and Contract.Requires<TException>(bool cond)?

To answer your first question, see section 2.1 Preconditions in the manual. Briefly, here is the difference:

Contract.Requires(bool cond)

This will throw a private Contract.ContractException exception if the condition evaluates to false. You cannot catch this exception (since it's private from your point of view)—this is to discourage catching and handling it, thereby making the contracts pretty much worthless.

Contract.Requires<TException>(bool cond)

If the condition evaluates to false, the specified TException will be thrown. You cannot use this form without running the contract tools on all builds.

About ccrewrite

Specifically, on page 20, in section 5. Usage Guidelines, it tells you all the different forms of contracts that Code Contracts can work with, how they work, and what the build requirements for each are.

I'll briefly summarize, but please, download the manual and read it. It's quite good, though not in any way complete—you have to do a lot of experimentation to learn how to effectively use Code Contracts. Also, if you have access to PluralSight, John Sonmez has a course called Code Contracts which is a great introductory course; and Michael Perry has an awesome course called Provable Code.

Contract Checking Is Not Required for Released Code

If you don't need contract checking in released code, then:

• Use Contract.Requires everywhere
• Enable Runtime Checking on Debug builds only.

Code Contract Checking is Required for Released Code

If you require contract checking on released code, you have two options:

1. Use Code Contracts "native" pre-conditions:
   • Use Contract.Requires<TException> on public API methods (e.g. methods that will be called by users of your library) for which you want to throw specific exceptions, e.g. ArgumentException.
   • Use Contract.Requires For non-public API methods or public API methods for which you don't want to throw a specific exception.
   • Enable Runtime Checking on all builds.
   • Ensure you enable options to only emit pre-conditions and only on public surface area of your assembly—e.g. only those methods that are callable by your library consumers.
2. Use "legacy" contract checking:
   • This is your old school style if (cond) { throw new Exception(...) } guard blocks on your public API methods
   • Use manual inheritance to enforce contracts on derived types. (When using option 1, Code Contracts can perform automatic inheritance of contracts from base classes, helping you avoid Liskov Substitution Principle violations.)
   • Make sure to place the line Contracts.EndContractBlock() after all your if (cond) { throw new Exception(...) } blocks so that Code Contracts knows these are your contracts.
   • On non-public API methods, you can feel free to use Contract.Requires for your contracts.
   • Enable Runtime Checking only on Debug builds.

One thing to note about the above: Contract checking is always enabled on Debug builds. If other developers on your team will be building this library, they will also need to have Code Contracts installed.

From Section 5.1.3: Forcing Projects to build with Contracts:

If you are using scenario 2 (Requires⟨Exn⟩) and you make your source code available to other developers, you might want to alert them that they need to use the tools to build your source. If so, you can insert the following snippet into your project file at the end (after the import of CSharp or VisualBasic targets):

<PropertyGroup>
<CompileDependsOn>$(CompileDependsOn);CheckForCodeContracts</CompileDependsOn>
</PropertyGroup>
<Target Name="CheckForCodeContracts"
        Condition="'$(CodeContractsImported)' != 'true'">
  <Error Text="Project requires Code Contracts: http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx" />
</Target>

Also, see Section 6.1: Assembly Mode where it tells you the difference between Custom Parameter Validation and Standard Contract Requires. This section makes it quite clear that the contract rewriter (ccrewrite) is always run on Debug builds.