Champion "Method Contracts"

[gafter]

• [ ] Proposal added
• [ ] Discussed in LDM
• [ ] Decision in LDM
• [ ] Finalized (done, rejected, inactive)
• [ ] Spec'ed

See also https://github.com/dotnet/roslyn/issues/119

[Lexcess]

Ok then I’ll bite.

First up, the common refrain is don’t worry Non-Nullable is coming, that’ll sort out 90% of your problems. With fresh eyes I'd like frame method contracts another way:

"Method Contracts are declarative definitions of method behavior that allow developers to define and follow consistent inline rules instead of disconnected documentation and unit/fuzzing tests."

I’m going to avoid talking syntax and implementation immediately because I think the initial conversation should be scope and vision. Previous threads seem to derail with some arguing over base concepts while others charged ahead with wildly differing syntax. However, I will lay out the key traits I’d like to see.

• Contracts should be declarative and defer choices on where, when and what guard code is emitted. e.g. public surfaces only, fail fast/exceptions.
  • Also, lets try to avoid weaving (please).
• Contracts should be terse and where possible applied via interface to reduce clutter.
• Contracts should not try to hide what is a runtime and what is a compile/static level check.
  • Clarity is the priority.
  • Ideally I'd like to see predicate style checks for the former and generic style constraints for the latter.
• Contracts should focus initially on a few key scenarios do them well and broaden out from there.
  • CC was a research project and it showed.
  • It tried to do too much and it was hard to pick up and harder to implement (esp. X-platform).

On that last point, obviously everyone has different ideas of the key pieces but for me they are:

• Pre-conditions (input or the old 'requires')
• Post-conditions (output or 'ensures')
• Predicate style runtime assertions
• Compile time constraints that can be statically inferred/checked
• Interface contracts
• Assertions such as: standard predicates (i.e. ranges, state checking), C#7 pattern matching etc...

I really liked CC and would love to bring forward our old code, but perfection is the enemy of good and I just don’t see CC coming over to .Net Core.

Everyone can start arguing about invariant again now :)

[MovGP0]

Here is a variation of the syntax that has been missed in the original proposal (taken from #511):

public void Foo(object o)
   requires o is Bar b else throw new ArgumentException(nameof(o)))
{
    // do something with `b`...
}

[Richiban]

If we're going to do this I'd absolutely love to be able to omit the else throw new ArgumentException(nameof(o))) where it's obvious.

public void Foo(object o) requires o is Bar b
{
    // do something with `b`...
}

is the same as this:

public void Foo(object o)
   requires o is Bar b else throw new ArgumentException(nameof(o)))
{
    // do something with `b`...
}

[alrz]

@Richiban if Foo requires o to be Bar it should have been declared as Foo(Bar o), unless it's an override or something, right?

[MovGP0]

@alrz It probably makes more sense for you to do something like this:

public void Foo(int age) 
    requires (age > 16) 
    else throw new ArgumentOutOfRangeException("Thou shalt not pass!", nameof(age)) 
{
    // ...
}

However, sometimes you need an object as a parameter, like when defining an event handler:

public void OnLeftButtonClick(object sender, MouseButtonEventArgs args)
    requires (sender is Control control) 
    else throw new ArgumentException("Wasn't a control.", nameof(sender))
{
    // ...
}

[Lexcess]

I'm not sure the value proposition is there if contracts boil down to moving existing guard code outside the method body.

I'd like to see something that is more strict, less magic and leverages existing c# terms and constructs. Namely:

• Use the same syntax as generics
• All clauses have to be generic Predicates (+maybe things like class reference type check?)
• Most implementation via a simple MethodContract static (extension) helper class
• Discuss whether custom contracts are desirable in an initial release (I would prefer having a model out there and extending rather than try and solve the world in one go)
• The syntactic sugar adds guard code inline, to make debugging/stack trace simpler.

So taking the above example:

public void Foo(int age) 
    where age : Range(0, 16)    
{
    // implementation...
}

We can then translate this into a predicate based on a helper method (and potentially any predicate... although I'm trying to keep it simple here) and then use some sort of compiler directive to say when guard code is generated (i.e. public methods only, debug only).

By default the above code be translated into something like:

public void Foo(int age) 
{
    // generated:
    if (MethodContracts.Range(age, 0, 16) == false)
    throw new OutOfRangeException(nameof(age), $"Acceptable range is {0} to {16}.")
    // implementation...
}

For return (ensures) values we can reuse the keyword return (which obviously wouldn't previously be valid here). The use of return means that we can avoid bringing in concepts such as requires and ensures.

public string Bar() 
    where return : NotWhiteSpace, MaxLength(10), HasUnicodeBom16()
{
    // implementation...
}

To somebody coming to the language fresh I think the idea that you can use the same syntax for generic constraints as well as method constraints makes a lot of sense. I've not talked about checks that apply outside the scope of the method here because: I'm not sure they are as valuable as we move towards side effect free code and I think they might be better served with a separate construct.

[TylerBrinkley]

@Lexcess I like the syntax, but how does the compiler know to throw an OutOfRangeException for the Range Method Contract? Shouldn't the Method Contract method return an Exception it would throw if the contract is not satisfied. So perhaps MethodContracts.Range would be specified as such.

public static Exception Range(int value, int inclusiveMin, int inclusiveMax);

Then the compiler would output the following for the example.

public void Foo(int age) 
{
    // generated:
    var exception = MethodContracts.Range(age, 0, 16);
    if (exception != null)
    throw exception;
    // implementation...
}

I use a variable name of exception here but it should be changed to something inexpressible in C# to prevent naming conflicts.

[Lexcess]

@TylerBrinkley That is a pretty neat solution. I was originally thinking you'd want to separate the predicate from the exception but if we assume that contracts are either applied by exception or non-existent (except perhaps by some documentation attributes) then it makes a lot of sense.

I'll think about it a bit more but it does significantly reduce what the compiler needs to know/do.

Also one thing from @MovGP0 I didn't address. On "is" checks. Ideally you'd simply change the method signature to the more specific type. Sure sometimes you don't own the signature, but I wonder if it is valuable enough to do the work to support a sub-optimal approach (you can still just do it in the method itself).

One thing I'd love to achieve here is that the syntax can be applied to interfaces and injected into implementations. If I saw even one person define an interface then have the contract define a subclass I'd feel like they were led down the wrong path. Interface support is the other reason I'd like to keep the contract options super simple, at least at first.

[MovGP0]

I disagree with the where and return syntax. The where is already used for type checking. It would be overkill to use it in too many contexts. As for the return syntax, you might want to do something like this:

public (int result, int rest) Divide(int numerator, int denominator) 
    require numerator > 0
    require denominator > 0
    ensure result > 0
    ensure rest >= 0
{
    // implementation...
}

For range checking, you could in principle do something like

require Enumerable.Range(16,120).Contains(age) 
    else throw new ArgumentOutOfRangeException("Must be between 16 and 119 years old.", age, nameof(age))

But it would be way less performant to enumerate and compare a few dozen numbers than to test just two inequalities:

require age >= 16 
    else throw new ArgumentOutOfRangeException("Must be at least 16 years.", age, nameof(age))
require age < 120 
    else throw new ArgumentOutOfRangeException("We do not accept mummies at this partey!", age, nameof(age))

[MovGP0]

if you want a range operator, consider an extension method:

public static bool IsInRange<T>(this T value, T start, T end)
    where T: IComparable<T>
{
    return value.CompareTo(start) >= 0 && value.CompareTo(end) <= 0;
}

and then you can use

require age.IsInRange(16, 119) else throw NewArgumentOutOfRangeException("...", age, nameof(age));

[Lexcess]

@MovGP0 interesting, would you not at least agree that a where constraint is a similar concept? I think it would aid discoverability, especially if you are new to the language.

The point on the extension methods isn't so much to shorten the line, it is a model for implementation. If you allow any code in the clauses you hit a couple of problems:

• How do you document from this
• You increase the risk of side effects
• What real value is there over having it inline?
• a lot more work to make sure the code generation works in all scenarios

For you tuple example I'd write similar syntax to parameters with:

public (string foo, int bar) FooBar() 
    where return foo : NotWhiteSpace, MaxLength(10), HasUnicodeBom16
    where return bar : Max(100)
{
    // implementation...
}

All that said, for me the key for Method Contracts/Constraints to have value is to be declarative. Otherwise you are just moving a block of code above the brace instead of below it.

[MovGP0]

@Lexcess contracts may not be attached to the functions/methods/procedures directly, but may be „clued“ on. Consider the following code (taken from here):

using System;
using System.Diagnostics.Contracts;

// implementation 
[ContractClass(typeof(IArrayContract))]
public interface IArray
{
    Object this[int index]
    {
        get;
        set;
    }

    int Count
    {
        get;
    }

    int Add(Object value);
    void Clear();
    void Insert(int index, Object value);
    void RemoveAt(int index);
}

// contract
[ContractClassFor(typeof(IArray))]
internal abstract class IArrayContract : IArray
{
    int IArray.Add(Object value)
        ensures return >= -1
        ensures return < ((IArray)this).Count
    => default(int);

    object IArray.this[int index]
    {
        get
            requires index >= 0
            requires index < ((IArray)this).Count
        => default(int);

        set
            requires index >= 0
            requires index < ((IArray)this).Count
        {
        }
    }
}

[MovGP0]

@Lexcess because of the declaritive approach:

I am unsure how something like

public (string foo, int bar) FooBar() 
    where return foo : NotWhiteSpace, MaxLength(10), HasUnicodeBom16
    where return bar : Max(100)
{
    // implementation...
}

should compile. Especially the MaxLength(10). Do you think about higher order functions there? Or about attributes that work like filters?

[Lexcess]

@MovGP0 Yes I use those a lot in the old contracts, but if we are modifying the compiler I'm thinking lets try and get a cleaner implementation here. That model was purely down to the restrictions of using post compile weaving.

On whether these are higher order functions, attributes or something else. I think this is something where we need to drive out what works best. My gut instinct is that higher order functions makes sense (perhaps fulfilling the signature as @TylerBrinkley described with a selection of typed parameters). However I could imagine cases where essentially they are special cased much like with the generic new() constraint.

I'm very aware that the CSharp team hasn't seemed very enthusiastic about contracts in the past, so I do think some weighting will have to be given to what is easiest to implement and test. This is also another reason I like the reuse of where, I'm hopeful some of the compiler code can be lifted and repurposed to achieve our goals rather than start from scratch.

[MovGP0]

@Lexcess my rationale is that functor attributes and higher order functions are harder to implement and harder to do interference with. I prefer the simpler solution in such cases.

[Serg046]

Even if higher order functions or attributes are harder to implement why not to use requires/where with @TylerBrinkley's approach? Why do we need to throw an exception manually each time of usage? I don't think it will significantly improve the readability.

[Flash3001]

Today where is restrictive, not allowing the code to compile in case the condition isn't meet. The reuse of the where keyword would force the caller to check the parameters? Or would it be a runtime exception, giving a double meaning to the word?

In any case, it would be nice to have static checks at compile time either as warnings or errors, not only exceptions or fail fast.

[Lexcess]

@Flash3001 I agree that static checks would be useful. I think trying to do the same amount of work in the compiler as the old static analyzer did is unrealistic but whatever can be done towards that would be beneficial.

Would you consider the fact that where is implemented as compile time only part of the 'contract' with the developer or is that just an implementation detail. I'd err more towards the latter. For example you could have an implementation of generic constraints that was extended to work with dynamic and I'd expect it to be a runtime check.

[MovGP0]

@Serg046 "Why do we need to throw an exception manually each time of usage?"

We don't. Contracts should be enforced at compile time. An error in the build log with the location of the calling code would be enough in such cases.

However, sometimes you might want to provide a better error message, so you should be able to override the default by providing a custom exception.

[MovGP0]

@Lexcess I find the where syntax confusing. require, ensure and assert keywords seem more consistent with established conventions:

• Eiffel: An Introduction to Design by Contract
• Spec# Example

[Flash3001]

@Lexcess, To be honest, I'm not sure!

I like the idea of where begin reused, as no new keywords need to be created and it has this logical sense of restricting input parameters - if generics is considered an input parameter.

My only issue with it would be the possible change of perceived meaning.

On the other hand what was done to is and switch to support pattern matching was an ingenious idea. The same idea could be applied to where so it would be extended in the same way, allowing compile and runtime checks of either generic, input or return.

I'm not advocating for any of the following samples, just an idea:

void Foo<T>(T parameter) where T : class // current behavior
void Foo<T>(T parameter) where T : class else throw AnyException() // change to runtime check and keep the contract
void Foo(int parameter) where parameter : Range(10, 100) // same as current behavior: force caller to check, otherwise do not compile.
void Foo(int parameter) where parameter : Range(10, 100) else throw AnyException() // runtime check

[MovGP0]

there is another reason. in cases where the return keyword is absent, it would not be clear when the constraint must be satisfied.

public static class Incrementor 
{
  public static int X { get; } = 0;

  public static void IncrementBy(int y)
    requires y >= 0; /* validate on start */
    ensures old(X) < X; /* does something at start; validates at return */
    ensures X >= 0; /* validate on return */
  {
    X += y;
  }
}

public void Foo(ref int bar)
    where bar > 0; // do you validate on start or on return? 
{
    
}

[TylerBrinkley]

@MovGP0 I was thinking about that and I think that would be a pre-condition.

The post-condition would be

public void Foo(ref int bar)
    where return bar: GreaterThan(0)
{

}

Obviously that would mean @Lexcess previous syntax for tuples wouldn't work anymore as there could be naming conflicts.

[Serg046]

void Foo<T>(T parameter) where T : class // current behavior void Foo<T>(T parameter) where T : class else throw AnyException() // change to runtime check and keep the contract void Foo(int parameter) where parameter : Range(10, 100) // same as current behavior: force caller to check, otherwise do not compile. void Foo(int parameter) where parameter : Range(10, 100) else throw AnyException() // runtime check

@Flash3001 Good suggestion. I like it but want to note that static checker can not be executed for each situation. What should be happened for this code? Nothing?

void SomeMethod()
{
    AnotherMethod(GetValueFromDb<int>());
}

void AnotherMethod(int value) where value: Range(10, 100)
{
    ...
}

I believe the code contracts must be a mix of static and runtime checks as it was implemented in CodeContracts

[MovGP0]

@TylerBrinkley how do you write the following?

public int Foo(ref int bar)
    require bar < 3;
    ensure bar > old(bar);
    ensure return > 0;
{
    // do something
}

[Richiban]

The where x : GreaterThan(0) actually makes it look quite a lot like dependent types. I wonder if that might actually be a more useful problem to solve than "just" method contracts;

E.g. (borrowing some syntax from F*):

public void Foo(int x { x > 0 })
{
    // Do something with x
}

[Lexcess]

@TylerBrinkley My thought exactly.

@Flash3001 Interesting. I guess my only concern (and this goes for @MovGP0 comments as well) is that I don't think we will get the kind of analysis and proofs that the old Code Contracts analyzer achieved in the compiler.

@Serg046

What do you think could be lifted from the static analyzer? My guess is very little. The analyzer was complex and struggled with edge cases (especially tracking side effects) . The compiler doesn't have that luxury. I loved the old analyser's features so I'd be glad to be wrong here.

@MovGP0 Something like:

public int Foo(ref int bar)
    where bar : Range(3, 4),
    where return : Min(0)
{
    // do something
}

@Richiban I actually think this is definitely an option of where this could go. This could offer a framework to reduce whole sets of what can only be done in unit tests these days: but in the method definition itself.

[MovGP0]

@Lexcess that range constraint doesn't solve the problem. try again.

[Lexcess]

@MovGP0 Apologies, I missed your ref. My gut instinct is that I wouldn't support a ref return constraint. Because ultimately it could be altered from another context so isn't provable.

If you still wanted to do it you'd just have where return bar after all you are just changing the name of the keyword. You might need to tweak the edge case of a Tuple that had the same name in it as a ref but otherwise it shouldn't be an issue.

[Flash3001]

@Serg046, In this case, it would have to be changed to a runtime exception or GetValueFromDb have the check applied to its return value - the same process we need to do today when inheriting from a generic class with where applied.

In practice, we can't predict a value coming from an external source, so either GetValueFromDb can't work and throw an exception, or it modify the value to fit the required output. The approach will change in each case.