Champion "Method Contracts"

[gafter]

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

See also dotnet/roslyn#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.

[Genbox]

@marinasundstrom
I discussed the problem of second-order/derived values with Professor Joseph Kiniry back in 2011. From what I remember, we came up with 5 different solutions, but they were in the context of "code correctness", and as such, even the body of a method had to follow the contract (and invariants would ensure the state of objects).

For example, a "full contract" solution means that the code is seen as a proof that has to be QED before it compiles. For example:

public int Add(int val1, int val2)
   ensures result <= int.MaxValue
{
   //This line would result in an exception when checked mode is turned on
   return val1 + val2; // <- this fails the contract. int.MaxValue + int.MaxValue is larger than int.MaxValue
}

public int Add(int val1, int val2)
   ensures result <= int.MaxValue
{
    Math.Clamp(val1, int.MinValue, (int.MaxValue -1) / 2); // <- can also be a require contract
    Math.Clamp(val2, int.MinValue, (int.MaxValue -1) / 2); // <- can also be a require contract
    return val1 + val2; // <- This now passes
}

This kind of contract is amazing for correctness, but difficult to implement, which is why Code Contracts had Contract.Require() on the incoming data, then normal data validation checks, and finally Contract.Assume() to satisfy the SMT constraints.

However, if we focus on pure API contracts and the second-order/derived values, only 2 solutions seemed to be viable. All examples below are a "require contract". Imagine [Requires("example here")].

Solution A: Explicit naming. That is the solution you have in your example. Example: "filename.Length <= 40"

• Pro: Easy to understand. Follows conventional thinking of C# developers
• Pro: Everything can be represented with the same structure. Example: "collection.Any(x=> x.Length == 4)"
• Con: Requires the spec analyzing (dynamic) code to understand arbitrary code. This is where contracts would overlap with runtime checks as you would need to know the value of "collection.Any(x=> x.Length == 4)" before you run the SMT solver.

Solution B: Macros. Imagine you have a macro to calculate the length of types. Example: "length(filename) <= 40"

• Pro: It is explicitly defined that we are working with the length of a structure. It can be any collection.
• Pro: While it looks like it runs at runtime, it does not. It is like changing the type of filename from string to stringOfMaxLength40. When the developer gives it "SomePath" it works just fine because it gets compiled to a stringOfMaxLength40 type. However, if it is longer than 40 characters, it will not compile to the type and compilation fails. Of course, like any other static analysis, it only works on constant data or when we can assume/require to satisfy the constraint
• Con: Requires developers to learn the macros. length(), max(), min() is just a subset of the required macros.
• Con: For length() to work on an arbitrary type, the developer would need to implement an interface. Code is not always available to do so.

[Clockwork-Muse]

but someone should at least try the simpler ones before ruling out its a bad idea.

The patterns or exact conditions representable aren't really the problem.

The biggest problem is the ecosystem - defining the compatibility of the ABI, dealing with NuGet packages, loading libraries with potentially conflicting/no info....
This isn't much of an issue if you commonly recompile the entire world (you only use the runtime, plus one or two updated package, to write an application). It's a major challenge when trying to deal with all the existing libraries out there, especially if they're stable and don't otherwise need to be recompiled (or can't, for any number of reasons).

[marinasundstrom]

@Clockwork-Muse Yes, that is why I propose the attributes approach just like with Nullable reference types. Letting you opt-in or out.

[marinasundstrom]

@Genbox Yea. I think there is a limitation to what we, realistically, can check and what expressions to allow.

We can mainly assure that locals and fields of primitive values are set to a certain value. Not evaluate that methods yield specific results.

There is a special case to this approach that I proposed:

The string literal “Foo” will yield a string instance that has a Length (3) annotated to it. It will help us make assumptions about that property.

After a local variable has received an instance of a string with a certain Length, I argue it should Ensure that any possible future assignments adhere to the same specification. The variable now has an Ensure attached to itself.

[Genbox]

@Clockwork-Muse

defining the compatibility of the ABI

That is not an issue, it is a feature. No really.

If a developer says "i need this input to be [1..10", but you have always given it 11 and it worked just fine, then you are relying on the developers good graces where he probably did something like if (val > 10) val = 10; //damn users.

When he updates the code with a contract that says requires val >= 0 && val <= 10 and your code suddenly no longer compiles, that is a good thing - you had a bug. Fix it to satisfy the contract.

potentially conflicting

Conditions just needs to be satisfied, so if one contract says requires val >= 0 && val <= 10 and another says requires val >= 0 && val <= 9, if the value is 5, both are satisfied. So what happens when the value is 10?

Well, not much. Your application won't compile, but the author declared his library won't work with a value of 10 anyway, so don't give it 10 or have them update their contracts. Today we mostly hope that it "just works", but if a library author explicitly declare that he does not support a value of 10, I'd much rather want to know it a compile-time than suddenly at run-time.

But lets say 10 is perfectly valid and the library author won't update his contract, then it shouldn't be that difficult to add an exception to the SMT solver so that particular check is not included. For example:

//Your code
static void Main()
{
   // Example 1 - Ignore contract for specific value
   Calculate(11!); // <- usually fails, but ! denotes that it is ignored (like with nullability)

   // Example 2 - Pragma warning disabled. Might disable multiple contracts on this line
   #pragma warning disable XXX
   Calculate(11); // <- usually fails, but pragma compiler directive ignores it

   // Example 3 - Explicit exclusion for code contracts
   #DisableContract(val)
   Calculate(11); // <- usually fails, but not for 'val' has it has been disabled
}

//Library code
public int Calculate(int val)
   requires val >= 0 and <= 10
{ }

@marinasundstrom have you thought about how to exclude one single requirement vs. disabling the analyzer for a whole line?

[marinasundstrom]

@Clockwork-Muse “ABI” will always break when you recompile. That is what happens all the time.

But at least it will not cause too much havoc, since this does not change the fundamentals of the CLR or the metadata. It is an opt-in compiler feature.

@Genbox No, I have not. That is worth thinking about.

We probably need to recognize parts that are not annotated too. Warn about passing a value from a source without a specification. And a way to tell the compiler that its OK.

[Clockwork-Muse]

Yes, that is why I propose the attributes approach just like with Nullable reference types. Letting you opt-in or out.

The fact that they're attributes don't make them optional.

That is not an issue, it is a feature. No really.

This assumes that everything is getting recompiled, and for that, I agree with you.
That is not the case for the wider ecosystem, especially when first released. People will want to be able to compile an app/library that uses/publishes contracts but depends on a library that doesn't. That's the harder part of the ABI/compat problem. In particular...

Conditions just needs to be satisfied

Assume that the conditions are from libraries that you pull in as dependencies, so you can't recompile the code. That's the actual issue here.

“ABI” will always break when you recompile. That is what happens all the time.

It doesn't actually. If this were the case, you couldn't update transitive dependencies until any other libraries using it were also update. Major library teams spend a lot of effort ensuring that they can publish patched binaries that are usable without recompiling other things that depend on them. It would mean that Windows Update would break all your applications.

Part of the "hard stuff" for this feature is even figuring out whether adding contracts at all would be a breaking change or not.

[rwv37]

"I'm very curious about those edge cases." There's an interesting page <https://nodatime.org/2.2.x/userguide/trivia> on the NodaTime website about stuff like this.

…

On 3/19/2022 4:48 PM, AlFas wrote: There have been months that have had 32 days. Minutes can be 61 seconds long. I'm very curious about those edge cases. your programming language may not allow you to represent things that are necessary. Either way, there can be similar constraints; I'm not the one to design the APIs, i.e. on dates. Whoever wrote the date APIs will take this feature seriously into consideration before applying it, let alone the how. — Reply to this email directly, view it on GitHub <#105 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB5RDQLK6YNK5RNNTG45CPTVAY4QHANCNFSM4DAESNBA>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Foxtrek64]

Just hoping to summarize this and make sure I got everything down. I believe we're in agreement that:

1. out and ref parameters are not supported (at least, insofar as this proposal).
2. The return keyword (as in ensures return is < 5) only applies to return values from functions and getters.
   1. Additionally, it should likely be in error to use ensures return on void methods.

There is still some debate on syntax. Major candidates appear to be:

• ensures for return values, requires for input parameters,
• where keyword to fit in with existing nomenclature.

Questions exist on whether it should be the responsibility of the developer to specify the exception, typical examples looking like requires condition else throw ....

Open questions -

How much do we want to link this into static analysis. For instance, would this open the door to allowing or type constraints or give us something similar to OneOf<T1, T2, ..., TN> parameters? Also, what are thoughts on mixing and matching contract styles? Take the following example:

// T must be a class and must either be of type Foo or type Bar.
public bool IsValid<T>(T t)
    where T : class
    requires T is Foo? foo or Bar? bar
{
    if (foo is not null)
    {
        // T is Boo
    }

    if (bar is not null)
    {
        // T is Bar
    }

    t.GetHashCode(); // Treat T as though it is `object`.
}

I'm sure the syntax can be cleaned up a bit here but I think it works well enough to show what I'm thinking.
Edit: Coming back to this a bit later - not sure I like the idea of variable declaration in the contract class as demonstrated above.
This would be much better done in the body a la if (t is Foo foo).

[marinasundstrom]

If I would have re-imagined C# as a language with method contracts. The use of keywords. And other changes.

public open class Calculator<T>
    extends Object 
    implements Disposable, AnotherInterface
    where T is not nullable
    where T implements Number
{
    public void Sqr(T value)
        requires value > 0
        ensure return > 0
        throws InvalidOperationException
    {
        return 0; // This will not be allowed as per "ensures". 
    }

    public void Dispose() 
    {

    }
}

Usage:

let calculator =  new Calculator<int>();

let r = calculator.Sqrt(2);  // Warning: InvalidOperationException not handled

let r = calculator.Sqrt(0);  // Warning: Not allowed as per "requires"

void Foo()
    throws InvalidOperationException
{
    let calculator =  new Calculator<int>();
    let r = calculator.Sqrt(2);  // No warning: InvalidOperationException to be handled by caller
}

Of course, I would rather use Result and Option types for application errors. But it would still apply for some stuff.

[jamescarter-le]

I know this has been attempted via Spec#, Boogie, CodeContracts and now this discussion, I believe a concerted effort from the language team to implement some static analysis to define method correctness would help bring C# back to the limelight where currently new developers are considering languages such as Go, with its GC, and Rust, with its 'managed' statically checked memory.

I've explored the various attempts at this on C# over the last 15 years, and whilst there have been good attempts made. I do think the core language team together with the MSR guys could create something amazing to allow people to build even more reliable systems in .NET. Projects like Coyote are examples of great work done to towards this end, but don't seem to make it into 'full fat' .NET

Many thanks to everyone working hard in this space, and helping to keep pushing C# into this new strange and highly competitive development ecosystem.

[douglasg14b]

A huge chunk of the developer ecosystem is adopting typescript, for example. Which enables devs to model their domains precisely, entirely via contracts, at compile time. Something C# simply cannot do without copious runtime, non-static, checks.

C# really needs to get with the game here, it's becoming clunkier and clunkier to use as a language. .Net carries C#, but the experiences of other languages is greater to such a degree that their own lack of 1st party frameworks or small standard libs is becoming less of a barrier when making ecosystem decisions.

[333fred]

@marinasundstrom this is not a repo for advertising other programming languages. Please keep issues on topic.

[marinasundstrom]

@333fred Understood.