BT

C# Futures: Method Contracts

| by Jonathan Allen Follow 576 Followers on May 18, 2015. Estimated reading time: 5 minutes |

For several years, developers have had the ability to add method level contracts via the Code Contracts research project. But this has a number of problems. It uses an imperative syntax that is verbose and poorly supported by tooling. To actually use the contract, both in the library and application, a post-compiler needs to be run. All in all it is an interesting project, but it needs first class compiler and syntax support to be useful.

Proposal 119, Method Contracts, seeks to offer this support. Like generic constraints, the pre- and post-conditions would be listed between the method signature and the body. Here is an example of what the syntax would look like:

public int Insert(T item, int index)
    requires index >= 0 && index <= Count
    ensures return >= 0 && return < Count
{ … }

There are three new keywords under this proposal. The phrase beginning with “requires” deals with pre-conditions. This is mostly going to be used for checking parameters, but in theory could also look at the state of the object itself. The keyword “ensures” is used for setting up post conditions. It would reuse the “return” keyword to refer to the result of the method call.

Fail Fast vs Exceptions

Like Code Contracts, this proposal was originally written to use fail fast. This is a rather aggressive form of contract enforcement where in any violation immediately crashes the application. Under this model, developers preferring to use exceptions would have to manually indicate it:

public int Insert(T item, int index)
    requires index >= 0 && index <= Count
        else throw new ArgumentOutOfRangeException(nameof(index))
    ensures return >= 0 && return < Count
{ … }

This part of the proposal has seen quite a bit of backlash.

Nathan Jervis writes,

You can know which parts of the program can't be affected and are safe to continue. There may be situations where you are writing critical code and maybe you do want fail fast, but I hardly think that it's impossible to know which part of your program failed.

It's just simply ridiculous to assume that the correct action would always be to kill the process immediately. If microsoft word had a bug when it saved to a network path because of a coding error, would you want it to immediately kill the app? No, you'd want it to save the file to a temporary location, give an error message to the user, log the problem, and then offer to try and restore the file when it loads next time.

HaloFour echoes that sentiment,

I think that it's absolutely silly for a contract violation on argument validation to cause the entire process to crash. Implementing it that way is a sure-fire way to guarantee that the feature is never used, at least by anyone writing anything non-esoteric. The point of that side of this feature is argument validation, and argument validation is inherently something from which the program can recover in some manner. And frankly, if it can't, the caller can make that decision by not catching the exception. This is how all implementations of code contracts that I've ever seen works on .NET now or in any other language.

David Nelson references the work on Code Contracts,

Having previously worked on Code Contracts, you are surely aware of the massive debate that went on there over whether or not to fail fast. The Code Contracts team tried for months (years?) to convince the community that failing fast was the right thing to do, but were ultimately unsuccessful. Having the opportunity to feel the effects of such a misguided decision, I certainly did not embrace it. I was one of those decrying the absurdity of fail fast then, and will continue to do so now.

Later he explicitly lists the problems that fail fast would cause

1) How do you do error logging? Watson is simply not sufficient; the vast majority of .NET applications don't use it because of the limited and arcane information it provides, and the difficult in accessing that information. EVERY .NET application I have ever seen produces its own error log.

2) Is it appropriate to take down a production web server serving millions of users around the world because of an innocuous logic bug in a corner case for one particular user?

3) What happens when a unit test violates a contract? Crash the unit test runner?

4) If a programming error should always instantly crash the process, why does every other error condition throughout .NET thrown an exception? Why does NullReferenceException even exist: shouldn't the process just die? Why does failing to JIT a method (which surely indicates a much more serious problem than a contract violation) throw an exception instead of killing the process?

Aaron Dandy likewise would like to see both options,

I would totally use fail fast, but I would like to be able to use that within my private surface. I really want exceptions for my public surface. I feel that if a user of my code decides to feed exceptions to the exception monster, that is their choice and they (implicitly, their users too) will deal with the consequences.

A concept that HaloFour agrees with,

I'd rather see method contracts throw exceptions (at least for the requires clause) and add a new language keyword assert to fail-fast if whatever condition is not met.

Types of Exceptions

The easy case in this proposal is the Argument exceptions. The compiler can easily turn a simple requires clause into an ArgumentNullException or ArgumentOutOfRange. If that requites clause instead looks at object state, it could throw an InvalidOperationException. But what it looks at both? Then determining which to throw could become quite complicated.

There is also the problem with ObjectDisposedException. There is no standard for representing a disposed object. Instead there is a very loose convention where in some Boolean field called _disposed or m_IsDisposed or something to that effect must be checked. This is important because InvalidOperationException is often recoverable by further changing the object’s state, while ObjectDisposedException never is.

On the back side, there needs to be an exception that indicates the ensures clause failed. Unlike requires, a failure of an ensures contract always means there was an internal bug in the method.

Localization

Assuming that an exception based approach is used, the next question that comes up is localization. For basic argument checks, the compiler can easily generate English text for an argument exception. But what happens when those exceptions needs to be localized for other languages? If using the abbreviated syntax where the argument exception doesn’t need to be explicitly indicated, there will need to be a backchannel where that information can be added. Or perhaps localization will require the verbose syntax.

Enums and contracts

Up until now, contracts have been merely additive. In this proposal by Fabian Schmied, the compiler can eliminate the need to add a return statement that should never be hit.

public enum MyEnum { One, Two, Three };|

public string GetText (MyEnum myEnum)
requires defined(myEnum)
{
    switch (myEnum)
    {
        case One: return "Single";
        case Two: return "Pair";
        case Three: return "Triple";
    }   
    // No error about missing return statement; all branches are covered.
}

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT