Invariant Contract

Purpose

This Code Provider adds the Invariant precondition to method parameter(s) or a variable assignment. The precondition ensures the passed or returned parameters are not empty throughout the method's life-cycle.

Availability

Available in the following cases.

  • When the caret is at the beginning of a method body. In this case, the contract will test all method parameters and strings.
  • When the caret is on a method's parameter name. In this case, the contract will test only the selected parameter.
  • When the caret is on a variable assignment.
Note

This Code Provider may be unavailable for variables of a non-nullable type, for instance, Integer.

Usage

  1. Place the caret at the beginning of a method body.

    Note

    The blinking cursor shows the caret's position at which the Code Provider is available.

    public void AddRecord(string name, object data) {
    //...
    }
    
  2. Use the Ctrl + . or Ctrl + ~ shortcut to invoke the Code Actions Menu.
  3. Select Add Contract | Contract.Invariant Contract from the menu.

After execution, the Code Provider adds the assumption statement against all the method parameters.

public void AddRecord(string name, object data) {
    Contract.Invariant(!string.IsNullOrEmpty(name), "name is null or empty.");
    Contract.Invariant(data != null, "data is null.");

    //...
}
Note

If the source file does not contain reference to the System.Diagnostics.Contracts namespace, the corresponding reference will be added.

See Also