Microsoft Code Contracts: Not with a Ten-foot Pole

After what seems like an eternity, a mainstream programming language will finally dip its toe in the Design-by-contract (DBC) pool. DBC is a domain amply covered in one less well-known language called Eiffel (see ISE Eiffel Goes Open-Source for a good overview), where preconditions, postconditions and invariants of various stripes have been available for over twenty years.

Why Contracts?

Object-oriented languages already include contracts; “classic” signature-checking involves verification of parameter counts and type-conformance. DBC generally means extending this mechanism to include assertions on a higher semantic level. A method’s signature describes the obligations calling code must fulfill in order to execute the method. The degree of enforcement varies from language to language. Statically-typed languages verify types according to conformance at compile-time, whereas dynamically-typed languages do so at run-time. Even the level of conformance-checking differs from language to language, with statically-typed languages requiring hierarchical conformance via ancestors and dynamically-typed languages verifying signatures via duck-typing.

And that’s only for individual methods; methods are typically collected into classes that also have a semantic meaning. DBC is about being able to specify the semantics of a class (e.g. can property A ever be false when property B is true?) as well as those of method parameters (can parameter a ever be null?) using the same programming language.

Poor-man’s DBC

DBC is relatively tedious to employ without framework or language support. Generally, this takes the form of using Debug.Assert[1] at the start of a method call to verify arguments, throwing ArgumentExceptions when the caller did not satisfy the contract. Post-conditions can also be added in a similar fashion, at the end of the funtion. Naturally, without library support, post-conditions must be added before any return-statements or enclosed in an artificial finally-clause around the rest of the method body. Class invariants are even more tedious, as they must be checked both at the beginning and end of every single “entering” method call, where the “entering” method call is the first on the given object. A proper implementation may not check the invariant for method calls that an object calls on itself because its perfectly all right for an object to be in an invalid state until the “entering” method returns.

One assertion that arises quite often is that of requiring that a parameter be non-null in a precondition. An analysis of most code bases that used poor-man’s DBC will probably reveal that the majority of its assertions are of this form. Therefore, it would be nice to handle this class of assertion separately using a language feature that indicates that a particular type can statically never be null. Eiffel has added this support with a separate notation for denoting “attached” types (types that are guaranteed to be attached to a non-null reference). Inclusion of such a feature not only improves the so-called “provability” of programs written in that language, it also transforms null-checking contracts to another notation (e.g. in Eiffel, objects are no longer nullable by default and the ?-operator is used to denote nullability) and removes much of the clutter from the precondition block.

Without explicit language support, a DBC solution couched in terms of assertions and/or exceptions quickly leads to clutter that obscures the actual program logic. Contracts should be easily recognizable as such by both tools and humans. Ideally, the contract can be extracted and included in documentation and code completion tooltips. Eiffel provides such support with separate areas for pre- and post-conditions as well as class invariants. All assertions can be labeled to give them a human-readable name, like “param1_not_null” or “list_contains_at_most_one_element”. The Eiffel tools provide various views on the source code, including what they call the “short” view, showing method signatures and contracts without implementation, as well as the “short flat” view, which is the “short” view, but includes all inherited methods to present the full interface of a type.

Looking at “Code Contracts”

Other than Eiffel, no close-to-mainstream programming language[2] has attempted to make the implicit semantics of a class explicit with DBC. Until now. Code Contracts will be included in C# 4.0, which will be released with Visual Studio 2010. It is available today as a separate assembly and compatible with C# 3.5 and Visual Studio 2008, so no upgrade is required to start using it. Given the lack of an upgrade requirement, we can draw the conclusion that this contracting solution is library-only without any special language support.

That does not bode well; as mentioned above, such implementations will be limited in their support of proper DBC. The user documentation provides an extensive overview of the design and proper use of Code Contracts.

There are, as expected, no new keywords or language support for contracts in C# 4.0. That means that tools and programmers will have to rely on convention in order to extract semantic meaning from the contracts. Pre- and postconditions are mixed together at the top of the method call. Post-conditions have support for accessing the method result and original values of arguments. Contracts can refer to fields not visible to other classes and there is an attribute-based hack to make these fields visible via a proxy property.

Abstract classes and Interfaces

Contracts for abstract classes and interfaces are, simply put, a catastrophe. Since these constructs don’t have method implementations, they can’t contain contracts. Therefore, in order to attach contracts to these constructs—and, to be clear, the mechanism would be no improvement over the current poor-man’s DBC if there was no way to do this—there is a ContractClass attribute. Attaching contracts to an interface involves making a fake implementation of that interface, adding contracts there, hacking expected results so that it compiles, presumably adding a private constructor so it can’t be instantiated by accident, then referencing it from the interface via the attribute mentioned above. It works, but it’s far from pretty and it move the contracts far from the place where it would be intuitive to look for them.

No Support for Precondition Weakening

Just as the specification side is not so pretty, the execution side also suffers. Contracts are, at least, inherited, but preconditions cannot be weakened. That is, a sub-type—and implementations of interfaces with contracts are sub-types—cannot add preconditions; end of story. As soon as a type contains at least one contract on one method, all methods in that type without contracts are interpreted as specifying the “empty” contract.

Instead of simply acknowledging that precondition weakening could be a useful feature, the authors state:

“While we could allow a weaker precondition, we have found that the complications of doing so outweigh the benefits. We just haven’t seen any compelling examples where weakening the precondition is useful.”

Let’s have an example, where we want to extend an existing class with support for a fallback mechanism. In the following case we have a transmitter class that sends data over a server; the contracts require that the server be reachable before sending data. The descendant adds support for a second server over which to send, should the first be unreachable. All examples below have trimmed initialization code that guarantees non-null properties for clarity’s sake. All contracts are included.

class Transmitter
{
  public Server Server { get; }

  public virtual void SendData(Data data)
  {
     Contracts.Requires(data != null);
     Contracts.Requires(Server.IsReachable);
     Contracts.Ensures(data.State == DataState.Sent);

     Server.Send(data);
  }

  [ContractInvariantMethod]
  protected void ObjectInvariant
  {
    Contract.Invariant(Server != null);
  }
}

class TransmitterWithFallback : Transmitter
{
  public Server FallbackServer { get; }

  public override void SendData(Data data)
  {
     // *contract violation*

     // If "Server" is not reachable, we will never be given
     // the opportunity to send using the fallback server
  }

  [ContractInvariantMethod]
  protected void ObjectInvariant
  {
    Contract.Invariant(FallbackServer != null);
  }
}

We can’t actually implement the fallback without adjusting the original contracts. With access to the code for the base class, we could address this shortcoming by moving the check for server availability to a separate method, as follows:

class Transmitter
{
  public Server Server { get; }

  [Pure]
  public virtual bool ServerIsReachable 
  { 
    get { return Server.IsReachable; }
  }

  public virtual void SendData(Data data)
  {
     Contracts.Requires(data != null);
     Contracts.Requires(ServerIsReachable);
     Contracts.Ensures(data.State == DataState.Sent);

     Server.Send(data);
  }

  [ContractInvariantMethod]
  protected void ObjectInvariant
  {
    Contract.Invariant(Server != null);
  }
}

class TransmitterWithFallback : Transmitter
{
  public Server FallbackServer { get; }

  [Pure]
  public override bool ServerIsReachable 
  { 
    get { return Server.IsReachable || FallbackServer.IsReachable; }
  }

  public override void SendData(Data data)
  {
    if (Server.IsReachable)
    {
      base.SendData(data);
    }
    else
    {
      FallbackServer.Send(data);
    }
  }

  [ContractInvariantMethod]
  protected void ObjectInvariant
  {
    Contract.Invariant(FallbackServer != null);
  }
}

With careful planning in the class that introduces the first contract—where precondition contracts are required to go—we can get around the lack of extensibility of preconditions. Let’s take a look at how Eiffel would address this. In Eiffel, the example above would look something like the following[3]:

class TRANSMITTER
  feature
    server: SERVER

    send_data(data: DATA) is
    require
      server.reachable
    do
      server.send(data)
    ensure
      data.state = DATA_STATE.sent;
    end
end

class TRANSMITTER_WITH_FALLBACK
  inherits
    TRANSMITTER
      redefine
        send_data
      end
  feature
    fallback_server: SERVER

    send_data (data: DATA) is
      require else
        fallback_server.reachable
      do
        if server.reachable then
          Precursor;
        else
          fallback_server.send(data)
        end
      end
end

The Eiffel version has clearly separated boundaries between contract code and implementation code. It also did not require a change to the base implementation in order to implement a useful feature. The author of the library has that luxury, whereas users of the library would not and would be forced to use less elegant solutions.

To sum up, it seems that, once again, the feature designers have taken the way out that makes it easier on the compiler, framework and library authors rather than providing a full-featured design-by-contract implementation. It was the same with the initial generics implementation in C#, without co- or contra-variance. The justification at the time was also that “no one really needed it”. C# 4.0 will finally include this essential functionality, belying the original assertion.

Thumbs Up or Thumbs Down?

The implementation is so easy-to-use that even the documentation leads off by warning that:

“a word of caution: Static code checking or verification is a difficult endeavor. It requires a relatively large effort in terms of writing contracts, determining why a particular property cannot be proven, and finding a way to help the checker see the light. […] If you are still determined to go ahead with contracts […] To not get lost in a sea of warnings […] (emphasis added)”

Not only is that not ringing, that’s not even an endorsement.

Other notes on implementation include:

• Testing frameworks require scaffolding to redirect contract exceptions to the framework instead of an assertion dialog.
• There is no support for edit-and-continue in contracted assemblies. Period. Contracting injects code into assemblies during the compile process, which makes them unusable for the edit-and-continue debugger.[4]
• Because of this instrumentation, expect medium to massive slowdowns during compilation; the authors recommend enabling contracts in a special build instead of in all DEBUG builds. This is a ridiculous restriction as null-checks and other preconditions are useful throughout the development process, not just for pre-release testing. Poor-man’s DBC is currently enabled in all builds; a move to MS Contracts with the recommended separate build would remove this support, weakening the development process.
• Some generated code (e.g. Windows Forms code) currently causes spurious errors that must be suppressed by manually editing that generated code. Such changes will be wiped out as soon as a change is made in the Winforms designer.

Because the feature is not a proper language extension, the implementation is forced within the bounds of the existing language features. A more promising implementation was Spec#—which extended the C# compiler itself—but there hasn’t been any activity on that project from Microsoft Research in quite some time. There are, however, a lot of interesting papers available there which offer a more developer-friendly insight into the world of design-by-contract than the highly compiler-oriented point-of-view espoused by the Contracts team.

This author will be taking a pass on the initial version of DBC as embodied by Microsoft Contracts.