Contents

Introduction
Design Goals
Embedding Checks
Packaging Contract Checks
Configuring Contract Checks
Conclusion
More Information

Introduction

The use of third-party components is helpful while writing complex software systems, but it can be difficult to debug software that interacts with third-party components. To address this problem, a mechanism for determining if one is using the component correctly would be beneficial. Reading component documentation may or may not help, depending on its clarity and precision. A formally specified contract for that component would be better, and would also allow run-time contract verification via assertions. The client of the component could enable these assertions during development and debugging, and then disable them for the final production release to increase performance.

This article presents nContract, a tool that provides configurable run-time contract verification without requiring component recompilation or source code access. nContract allows component developers to formally specify .NET components using attributes. This contract information is retrieved from the compiled component’s metadata and a subclass is generated for each formally specified type. All members of the component’s interface are overridden and contract assertions are wrapped around calls to the base class. As long as the component client uses a factory to create instances of the component’s types, the decision of whether or not to create assertion-checked or unchecked objects can be deferred until run-time.

nContract Overview Diagram
Figure 1: Overview of nContract.

Design Goals

  1. Contract information is embedded in the binary version of the component.
  2. Run-time checks can be added or removed without recompilation of either component or client code.
  3. Checks can be enabled or disabled at the assembly, class or method level.
  4. Checks can be enabled or disabled individually on a pre-, post-, exceptional postcondition and class invariant level.
  5. Little or no performance penalty occurs if checks are disabled.
  6. Custom actions can be performed on contract violations.

Embedding Contracts

NET components are self-describing; all the information needed to describe the component is stored as metadata in the binary component. On top of this, .NET allows for developers to add custom metadata to the component by using custom attributes. Attributes are tags that can be added to code constructs such as classes, methods, parameters and other constructs where custom information needs stored. Here is a simple code example that has a FormallySpecified attribute attached to the class and a Pre attribute attached to the method:

[FormallySpecified]
public class Test {
  [Pre("i > 0")]
  public void DoWork(int i) { }
}

.NET provides a reflection API that allows programmatic retrieval of component metadata at run-time. By using attributes to store the DbC contract information, the contract can be retrieved from the binary component, eliminating any need for source code access. Furthermore, precise written documentation can be generated by pulling the contract information out of binary components.

nContract provides a set of attributes that are used to store the DbC contract information such as preconditions and postconditions for methods. These conditions are expressed as a string parameter given to the attributes. These condition strings are extracted by the nContract tool and inserted in a code template to generate run-time checks. Since run-time checks will be compiled as C# code these condition strings must be C# boolean expressions (other .NET languages could be used for the expressions if the templates were changed to that particular language). Here are the contract attributes and a brief description of each:

  • FormallySpecified – Marks a class as being formally specified.
  • Pre – Provides a condition which needs to hold true on the entry of a method.
  • Post – Provides a condition which needs to hold true on the exit of a method.
  • ExceptionalPost – Provides a condition which needs to hold true whenever the specified exception is thrown from a method.
  • Invariant – Provides a condition which needs to hold true after an object's creation and before and after every public method call for that object.
  • RepresentationalInvaraint – Same as invariant except it is not part of the public specification. Its purpose is for a developer to provide invariants which reference internal data and can be verified at run-time by nContract.
  • ModelField – An abstract field a developer can use for public specification which allows them to change implementation details later without breaking the public specification.
  • Pure – Marks a method as having no side effects. Any method that is used in any of the condition expressions needs to be marked as pure.

Below is an example of a formally specified class using the attributes listed above:

[FormallySpecified]
[ModelField(typeof(List<char>), "Contents",
  @"new List<char>(this.ToString().ToCharArray())")]
[RepresentationalInvariant("numberOfChars == stringBuilder.Length")]
public class CharBuffer 
{
  [Pre("value != null")]
  [Post("Contents.Count == value.Length")]
  protected CharBuffer(string value) { }

  ...

  [Pre(@"index >= 0 && index <= Contents.Count && value != null")]
  [Post(@"Contents.Count == old.Contents.Count + value.Length")]
  [ExceptionalPost(typeof(ArgumentOutOfRangeException),
    "index < 0 || index > Contents.Count")]
  public virtual void Insert(int index, string value) { }

  ...
  
  // Member fields 
  protected StringBuilder stringBuilder;
  protected int numberOfChars;
}

By using subclasses to package run-time checking code there are a number of design restrictions that a component developer needs to keep in mind:

  1. In order to inherit from a class, the class cannot be private nor can it be sealed or static.
  2. All the constructors that are to be checked at run-time must be public or protected. To ensure that the client uses a factory method instead of the new operator it is recommended that the component developer make all the constructors protected
  3. All methods or properties that are to be checked at run-time must be public or protected and they must also be overridable. To be overridable the method or property must either have a virtual or override keyword associated with it. static and private methods or properties are not checked because they cannot be overridden.
  4. Fields are not checked. To get around this limitation one could create a public or protected virtual property that references the field in question. If a field is used in any of the contract conditions it must be at least protected otherwise it will not be accessible to the subclass.
  5. The new operator cannot be used to create objects; a factory method must be used instead.

Using a factory method allows the decision to create an instance of the class with or without embedded checks to be made at run-time. The component developer has two primary choices for the factory method: use a generic factory method or create custom factory methods for each constructor in the formally specified class. The generic factory method, seen in the code sample below, creates an instance of the checks embedded subclass if checks are enabled for a particular type, or creates an ordinary instance if the checks are not needed.

public static T Create(params object[] args) {
  if (ChecksEnabled())
    return CreateChecksEnabledInstance(args);

  return (T)System.Activator.CreateInstance(typeof(T),
    BindingFlags.Public | BindingFlags.NonPublic |
    BindingFlags.Instance | BindingFlags.CreateInstance,
    null, args, null);
}

This generic factory method requires the least amount of work from the component developer but may require a larger learning curve for the client. One of the problems with making the factory method completely generic is that it uses the dynamic method Activator.CreateInstance to create the objects. Creating objects dynamically tends to be slower than creating them using the static new operator. Another downfall is that the parameters are not strongly typed so the compiler cannot catch potential type errors of the parameters being passed.

The other approach for the component developer is to create a custom factory method for each constructor in the formally specified class. This eliminates the problem of strongly typed parameters and also allows for the static new operator to be used in the normal case (i.e. when checks are disabled) which make it more efficient. Here is a sample custom factory method:

public static ClassName Create(PT1 p1, PT1 p1) {
  if (Factory<ClassName>.ChecksEnabled())
    return Factory<ClassName>.CreateChecksEnabledInstance(p1, p2);
  return new ClassName(p1, p2);
}

This is one example of a potential custom factory method; there could be others that optimize things like the creation of the object with checks embedded.

Packaging Contract Checks

For every formally specified type in a given .NET component nContract uses a template to generate a subclass for that type. In this subclass a constructor and a factory method with the same parameter profile is generated for every public or protected constructor in the formally specified class. This factory method allows for the preconditions to be checked before the call to constructor and it also allows for the exceptional postconditions to be checked. Here is a simplified example constructor and factory method:

public CharBufferWithChecks(string value) : base(value)
{    
  if(config.ctor_String.PostDisabled == false)
    config.CheckPostcondition(Postcondition);

  if(config.ctor_String.InvariantDisabled == false)
    config.CheckExitInvariant(InvariantCondition);
}
public static ExampleComponent.CharBuffer Create(string value)
{
  if(config.ctor_String.PreDisabled == false)
    config.CheckPrecondition(Precondition);

  CharBufferWithChecks newObject = null;
  try
  {
    newObject = new CharBufferWithChecks(value);   
  }
  catch(Exception ex)
  {
    if(config.ctor_String.ExceptionalPostDisabled == false) {
      if(ex is ExceptionType) {
        ExceptionType excep = ex as ExceptionType;
        config.CheckExceptionalPostcondition(ExceptionalPostcondition);
      }
    }
    throw;    
  }  
  return newObject;
}

Also every public or protected virtual method or property from the formally specified class is overridden in the subclass and assertion checks are inserted around calls to the base method or property. Here is a simplified example of a method:

public override void Insert(System.Int32 index, System.String value)
{
  if(config.Insert_Int32_String.InvariantDisabled == false)
    config.CheckEntryInvariant(InvariantCondition);

  if(config.Insert_Int32_String.PreDisabled == false)
    config.CheckPrecondition(Precondition);

  try {
    base.Insert(index, value);
    if(config.Insert_Int32_String.PostDisabled == false)
      config.CheckPostcondition(PostCondition);
  }
  catch(Exception ex) {
    if(config.Insert_Int32_String.ExceptionalPostDisabled == false) {      
      if(ex is System.ArgumentOutOfRangeException) {
        System.ArgumentOutOfRangeException excep = ex as System.ArgumentOutOfRangeException;
        config.CheckExceptionalPostcondition(ExceptionalPostcondition);
      }
    } 
    throw;    
  }
  finally {
    if(config.Insert_Int32_String.InvariantDisabled == false)
      config.CheckExitInvariant(InvariantCondition);
  }
}

A similar template is used for the overridden properties. The only other items that are included in the subclass template are properties that represent the model fields and a reference to the associated configuration class (i.e. the config variable in the templates above). Note that these template examples are simplified for understandability; the actual template is done using CodeSmith and it can be found in the nContract download.

Configuring Contract Checks

To provide appropriate flexibility to clients, nContract gives them the ability to individually configure precondition, postcondition, exceptional postcondition and invariant checks at the assembly, class and method level. In order to do this efficiently nContact also uses a template to generate a custom configuration class for every formally specified class. Here is a simplified example of a configuration class:

public class CharBufferConfiguration : ContractSpecification.ClassConfiguration
{
  public static CharBufferConfiguration GetConfig() {
    return Factory<ExampleComponent.CharBuffer>.GetConfig() as CharBufferConfiguration;
  }
  public CharBufferConfiguration() : base(typeof(ExampleComponent.CharBuffer)) { }

  public ContractSpecification.MethodConfiguration ctor_Void;
  ...
  public ContractSpecification.MethodConfiguration Insert_Int32_String;
  ...
}

By generating a custom configuration class a field can be generated for every constructor, method and property which contains the settings for the individual check types. This allows these configuration settings to be directly referenced in the generated subclass which makes it very efficient to determine if a particular check type is disabled for a particular method.

Once all these subclasses and configuration classes are generated then nContract compiles them into another .NET assembly. This .NET assembly is loaded and an instance of each configuration class is created. These configuration classes are then serialized to an XML file to control the settings for that assembly. Here is the XML configuration file that corresponds to the configuration class above:

<?xml version="1.0" encoding="utf-8"?>
<ArrayOfClassConfiguration
  xmlns:xsi=http://www.w3.org/2001/XMLSchema-instance
  xmlns:xsd="http://www.w3.org/2001/XMLSchema">
  <ClassConfiguration 
    xsi:type="CharBufferConfiguration"   
    TypeName="ExampleComponent.CharBuffer" 
    Enabled="true" UseDefaultTraceAssert="true">

    <ctor_String PreDisabled="false" PostDisabled="false" 
      ExceptionalPostDisabled="false" InvariantDisabled="false" />
    ...
    <Insert_Int32_String PreDisabled="false" PostDisabled="false" 
      ExceptionalPostDisabled="false" InvariantDisabled="false" />
    ...
  </ClassConfiguration>
</ArrayOfClassConfiguration>

Now configuring the checks becomes as simple as modifying this XML file. For example if one wishes to disable all checks for the CharBuffer class they just need to set the Enabled attribute on that class to false. Similarly this can be done for disabling particular check types for a given method.

Conclusion

Having configurable run-time contract verification can provide a great tool for component developers and clients. It adds an extra layer of verification that allows component developers to ensure their component does what it is supposed to do given the correct input. For clients it helps alleviate the problem of not knowing the correct input and expected output for a particular component. By having this verification when the client uses a component they are more likely to produce more reliable software systems with that component. Using nContract allows component developers and clients to get the benefit of run-time contract verification with the added ability to disable it without performance penalty, all without source code or recompilation.

More Information

Post your questions or comments in the nContract forum or contact me directly via my contact form on my weblog.

For more details on nContract you can download my thesis and/or the nContract Source Code.
Downloads: nContract-Thesis, nContract Quick Start nContract Source CodeVT ETD digital library entry