Home > Articles > Contract Programming in .Net

Articles

Contract Programming in .Net

Design by Contract (DbC) or Programming by Contract is an approach in designing computer software. It prescribes that system components (similar to classes in object-oriented programming) collaborate with each other by agreeing on contracts, on the basis of mutual obligations and benefits. The term was introduced by Bertrand Meyer in connection with his design of the Eiffel programming language in 1986. Contract programming enables better software reliability and provides a basis for specifications, documenting and testing.

In relations between people or companies, a contract is a written document that serves to clarify the terms of a relationship. It is really surprising that in software, where precision is so important and ambiguity so risky, this idea has taken so long to impose itself. […] Perhaps the most distinctive feature of contracts as they occur in human affairs is that any good contract entails obligations as well as benefits for both parties — with an obligation for one usually turning into a benefit for the other. This is true of contracts between classes, too.
Bertrand Meyer, Object-Oriented Software Construction, 2nd Edition, 2005

Introduction

 In the terms of contract programming, the calling method is a client (it uses a certain service provided by the supplier) while the called method is a supplier (it provides a certain service to the client).

This is an example contract for the Remove method of the ContractedStack class from the example project created for this article:

Obligations for the client (and benefits for supplier) are preconditions. They are requirements that must be met by the client to use a certain service. Benefits for the client (and obligations for the supplier prescribing what the supplier should do after the client has satisfied its obligations) are postconditions. Apart from preconditions and postconditions, the contract definition includes class invariants that apply to the class as the whole. Class invariants should be satisfied after calling any constructor of the class, methods of the class should preserve the invariant.

A method’s precondition describes its requirements that should be satisfied by its clients. In the example above, the Remove method can be called only when the stack is not empty. The requirements defined in the precondition need not be verified in the code of the method, this should be done by the client. The paradox is that contract programming can enhance code reliability by reducing the number of explicit checks in the code itself.

A method’s postcondition describes conditions that must always be true after the execution of the method (i.e. guaranties for the client, given that previously the client has met the method’s preconditions).
The class invariant is a set of properties that each component of the class must have. They should be satisfied after calling any constructor of the class and should be added implicitly to every pre- and postcondition of every public method. Class invariant guaranties consistency of the class components through the whole lifecycle of the object. Temporary breaking the class invariance during the method calls is possible, but should be reinstated after each method call.

Inheriting
When classes are inherited, their contracts are also inherited. Generally, when inheriting, the following rules are followed to merge contracts of the parent and child:

  • Preconditions are weakened — parent's assertions are ORed with those of the inheriting class
  • Postconditions are strengthened — parent's assertions are ANDed with those of the inheriting class

In the Microsoft Code Contracts library described in detail below weakening of preconditions are not allowed and defining preconditions in inheriting classes is forbidden.

Extra
When executing the code, contract verification can be enabled or disabled at the level of software module.

It should be kept in mind that contracts can not be used to verify data input by user, another program, operating system etc.

Benefits of Contracts

  • Contracts are useful from the methodological point of view — they can help further clarify logical assumptions behind system components and their behavior.
  • Contracts are indispensable to documenting software. Using contracts along with method signatures and XML descriptions provides additional info on requirements and guaranties of classes, which further ensures code stability.
  • Contracts can be verified while executing draft versions of software and then contract verification can be switched off in its final version.
  • Contracts help abandon defensive programming techniques when creating an application whose components interact with each other.
  • Contracts provide a basis for static class authentication utilities, automatic test utilities, runtime checking etc. These can automate building reliable applications.
  • Contracts can be used in object-oriented analysis and design. At the meeting with a customer, an analyst can make a sketch of the key classes of the future application, define their connections and methods, provide them with contracts. These abstract classes and interfaces can be further used by developers by inheriting classes of business objects.

Microsoft Code Contracts

For .Net languages Microsoft created the Microsoft Code Contracts library and toolset which allow using contact programming irrespective of its support by the programming language.

Help topics and detailed information are available at:

Installation

In .Net 4, the library is included in the Base Class Library (BCL).
.Net Framework 3.5 users can download the library and utilities from:

  • The Code Contracts project page on DevLabs  http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx. Code Contracts on DevLabs is for commercial use and available in Standard and Premium editions. Standard version can be installed on any edition of Visual Studio except Express. Premium version contains an extra utility for static contract analysis and can be used only with VS 2008 Team System, VS 2010 Premium or Ultimate preinstalled.
  • Microsoft Research page http://research.microsoft.com/en-us/projects/contracts/default.aspx. CodeContracts on Microsoft Research is intended for academic use only (for example, for students) and requires VS 2008 Professional or higher.

Setup

The simplest way to setup the library is to use the add-in provided along with Code Contracts. It creates an additional Code Contracts tab of the project properties page.

Check the Perform Runtime Contract Checking and choose the statement verification level: Full, Pre and Post, Preconditions, ReleaseRequires, None.

If, for some reason, this page is unavailable, do the following to make minimal contract statement verification:

1) Add CONTRACTS_FULL as a value of the Conditional compilation symbols parameter on the Build tab on the project properties page.

2) Set up handling of the code by the ccrewrite.exe module. To do so, on the Build Events tab in Post-build event command line add ccrewrite.exe $(TargetFileName) (it is assumed that the path to ccrewrite.exe was already stated in the PATH environment variable).

Utilities

Along with the library, a set of utilities is provided to support contract programming in .Net. In fact, controls on the Code Contracts tab provide GUI to use the key functions of the utilities. To find out details, learn their capabilities:

  • Ccrewrite. This utility post-processes the compiled IL code. As a result, contract conditions are turned into method calls to verify contract statements;
  • Cccheck. This tool performs static verification (while compiling) of the code correctness in terms of contracts;
  • Сcrefgen. This tool extracts all contracts into a separate assembly. This is convenient for separate delivery of the library assemblies without including contracts (for better performance) and with contracts, to be used by other developers;
  • Сcdocgen. Based on the contract-containing assembly, this tool adds contracts to XML documents. Supports the SandCastle project (automatic documenting of assemblies in a MSDN-like way).

Using Microsoft Code Contracts

In .Net 3.5, before start working, it is needed to add a link to the Microsoft.Contracts assembly to the project. In .Net 4, the assembly is added to the Base Class library.
Library classes occupy the name space System.Diagnostics.Contracts.

Declaring Preconditions

Preconditions are declared by calling:

  • Contract. Requires (Boolean)
  • Contract. Requires (Boolean, String).

Calls are placed at the start of the method:

public MyStack(int n)
        {
            Contract.Requires(n >= 0, "Positive capacity");

To add contracts to an existing application, where external parameters are already inexplicitly checked in the If-Then-Throw form, use the Contract. EndContractBlock() call. It informs the executing environment that all these structures before it are preconditions.

if (input == null) throw new NullReferenceException();
    Contract. EndContractBlock();

If new statements are added in the form of the Contract.* calls after the If-Then-Throw part, the above code will be automatically turned into a precondition and it is not needed to call EndContractBlock.

Declaring Postconditions

Posconditions are declared by calling:

  • Contract.Ensures(Boolean)
  • Contract.Ensures(Boolean, String)

Calls are placed at the start of the method, typically after preconditions.

Contract.Ensures(Capacity == n);

In postconditions, the following methods can be used:

  • Contract.Result() value returned by the method
  • Contract.OldValue(T input parameter) value of the input parameter before calling the method

Contract.Ensures(Count == Contract.OldValue(Count) + 1, "One more item");

Declaring Class Invariants

All class invariants are located in a dedicated class method. This method must contain only definitions of class invariants and marked with the attribute ContractInvariantMethod. Naming this method ObjectInvariantis is one of the best practices.

[ContractInvariantMethod]
protected void ObjectInvariant()
{
   Contract.Invariant(0 <= Count, "Count non negative");
}

Contract Violation Handling

When contract verification is enabled, it is important to address contract violation properly. Code Contracts provides the following capabilities for this:
If no standard handler is defined, first the handler of the ContractFailed event will be called for. If it is not found, or the handler cannot set the event as handled, the Contract.Failure method will be called. Implementation of this method is modified with every version. At the moment, if on the Code Contracts tab the box Assert On Contract Failure is checked, then the Debug.Assert method will be called, otherwise an exeption of the ContractException type will be thrown.

The Contract.ContractFailed event has the following signature:

public static event EventHandler ContractFailed;

where ContractFailedEventArgs are defined as follows:

public sealed class ContractFailedEventArgs : EventArgs
    {
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        public ContractFailedEventArgs(ContractFailureKind failureKind, string message, string condition, Exception originalException);

        public string Condition { get; }
        public ContractFailureKind FailureKind { get; }
        public bool Handled { get; }
        public string Message { get; }
        public Exception OriginalException { get; }
        public bool Unwind { get; }

        [SecurityCritical]
        public void SetHandled();
        [SecurityCritical]
        public void SetUnwind();
    }

When using the contract violation handler, it should be registered as early in the executable code as possible. The right point is the event of assembly initialization.

An example of registering a handler for projects similar to Test Project:
        [AssemblyInitialize]
        public static void AssemblyInitialize(TestContext testContext)
        {
            Contract.ContractFailed += (sender, eventArgs) =>
            {
                eventArgs.SetHandled();
                eventArgs.SetUnwind();                 
                Assert.Fail(eventArgs.Message);
            };
        }

Special Cases

When creating contracts, you are sure to experience such difficulties as compilation errors while declaring preconditions in structure constructors or declaring preconditions for methods’ input parameters, inability to define contracts for GUIs and others. Similar cases and resolution tips are described in the library documentation (http://download.microsoft.com/download/A/1/2/A1220EB5-7CDD-403D-B94A-EEDFFA1848EB/userdoc.pdf)

Present and Future of Contract Programming

Contract programming has just started its way across .Net languages. I suggest learning the Sec# language and following its progress (http://research.microsoft.com/en-us/projects/specsharp)  — it is based on C# and has a built-in support of contracts. Probably, many of its contract features will be added to a new version of C# in the future.

Also, numeral articles on contract programming were written by the Eiffel programmers community. In Eiffel, contracts have been used since 1986, and abundant practices and examples have been accumulated since then. The syntax of the language is simple and can be understood without special training. Apart from this, getting acquainted with the source code of standard libraries at ISE Eiffel Studio (http://dev.eiffel.com) is useful — it contains a wiki for developers, with links to a repository of the source code and latest versions of the product itself. Documents can be found at http://docs.eiffel.com/.
Eiffel Studio can compile both C and .Net code with its further compilation into an executable module. Also, an add-on to Visual Studio is available that enables writing code in Eiffel.Net and taking advantage of standard contract libraries of this language. The code of open-source libraries for this language is also available:  http://www.gobosoft.com/.

To gain a better understanding of contract programming and its purposes, to hone your contract writing and create clear and unambiguous contracts, you can follow contract programming innovations described in the research papers of Chair of Software Engineering of Swiss Federal Institute of Technology Zurich (ETHZ) http://se.inf.ethz.ch/research/index.html.

If these technologies are applied, the following scenario will come true in the foreseeable future:

  1. Programmer writes code.
  2. A code correction tool finds a defect and creates a counterexample (e.g. «Postcondition is not satisfied in the case of the following values of the fields of the class and the following input parameters of the method: …»).
  3. Based on the counterexample, a utility generates a failure test case.
  4. Based on the failure test case, an automatic correction utility suggests possible ways to fix the defect in the code.
  5. An automatic testing utility tests the suggested solution and checks execution. If successful, the solution is suggested to the programmer.

Links

Maxim Pankov