[Draft] Code Contract Compiler Warnings and Errors

Code Contract compiler issues errors and warning if the user violates some rules. This document will show a list of warnings and errors produced by Code Contracts as well as some new warnings that ReSharperContractExtensions will show.

Inconsistent Visibility in preconditions

Design by Contract has a rule for preconditions: all members mentioned in a contract must be at least as visible as the method in which they appear. This is true for Eiffel, this is also true for Code Contracts library.

Code Contract compiler will show following errors when it detects violation of this rule:

Using less-accessible members in the Contract.Requires

private bool _isValid;
public void Foo()
{
  // error CC1038: Member 'Sample._isValid' has less visibility than 
  // the enclosing method 'Sample.Foo'.
  Contract.Requires(_isValid);
}

The same is true when calling less visible method from the Contract.Requires (like bool Validate()). Unfortunately, Code Contract will not show an error for accessing private property and following code successfully compiled by Code Contract compiler:

private bool IsValid {get; set;}
public void Foo()
{
  Contract.Requires(IsValid);
}

I assume that this is a bug in Code Contract and this tool will show an error in the IDE in this case as well.

Using less-accessible members in the Custom Parameter Vlaidation block

The same accessibility rule is applied for any kind of preconditions:

• For Contract.Requires (covered in the previous section);
• For if-throw followed by Contract.EndContractBlock;
• For guard-methods marked with ContractArgumentValidator.

Unfortunately Code Contract compiler will not warn about last two cases, but ReSharperContractExtension will warn!

Exception for access-visibility rule: ContractPublicPropertyName

(For more information, see section 4.5 at the code contracts documentation at http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf)

Contract.Requires could use fields marked with ContractPublicPropertyName:

[ContractPublicPropertyName("IsValidProp")]
private bool _isValidField;
public bool IsValidProp { get; set; }
public void Foo()
{
  Contract.Requires(_isValidField);
}

Code Contract compiler will emit an error if ContractPublicPropertyName will point to the non-public field or property, or to undefined field/property. I.e. following code will produce a compile-time error from Code Contract compiler:

// error CC1010: Field 'Sample._isValidField' is marked [ContractPublicPropertyName("IsValidProp")], 
// but no public field/property named 'IsValidProp' with type 'System.Boolean' can be found
[ContractPublicPropertyName("IsValidProp")]
private bool _isValidField;
private bool IsValidProp { get; set; }
// The same error would be if the attribute would have: "IsValid"

Rules for message arguments for Contract.Requires

Contract.Requires contains second optional argument: message. Code Contract library allows to use only static fields/properties with (at least) internal visibility, otherwise error would be issued:

private string _message = "foo"; public void Foo() { // error CC1065: User message to contract call can only be string literal, // or a static field, or static property that is at least internally visible. Contract.Requires(false, _message); }

Rules for contract blocks

There is a few critical rules for contract blocks. The contract block itself is not clearly defined in the Code Contracts documentation, but there are some basic rules.

Classical contract block: set of Contract.Requires and Contract.Ensures statements or Old-style contract block: set of if-throw or if-guard statements followed by Contract.EndContractBlock().

There is some rules that user should follow when define contract block of the method.

Error: Calling a void-return method in the contract block

public void Foo()
{
  // error CC1027: Malformed contract.
  System.Console.WriteLine();
  Contract.Requires(false);
}

The same error would be issued for calling any other void-return methods: instance/static method of the same type, instance/static method of any other types.

Exception for previous rule: ContractArgumentValidator

The only exception for previous rule is to call a method marked with ContractArgumentValidator:

static class ContractValidator
{
    [ContractArgumentValidator]
    public static void Guard(bool condition)
    { }
}
class Sample
{
  public void Foo(string s)
  {
    ContractValidator.Guard(s != null);
    Contract.EndContractBlock();
  }
}

Another exception: pseudo-old-style preconditions

Code Contract allows to call any void-return method in if blocks (without requirements ContractArgumentValidatorAttribute):

public bool IsValid {get; private set;}
public void Foo()
{
  // if-method call is treated as a custom parameter validation
  if (IsValid)
    SomeInstanceMethod();
  Contract.EndContractBlock();
}

Error: precondition/postcondition checks after EndContractBlock

Contract.EndContractBlock means the end of the contract section so any other precondition/postconditions considered as an error:

public void Foo(string s)
{
  Contract.EndContractBlock();
  // error CC1012: Contract call found after prior EndContractBlock.
  Contract.Requires(s != null);
}

Errror when Contract.Requires is after Contract.Ensures

Following code will produce a compilation error:

public void Foo()
{
  Contract.Ensures(false);
  Contract.Requires(true);
}

Interestingly enough that Code Contract compiler will not even warn for Contract.Ensures after any other forms of preconditoins like if-throw or calling guard methods (marked with ContractArgumentValidator).

Error for assignment statements in the contract block

Not existing warnings

New warnings

Invariants

CodeContract and CodeContractFor attributes