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.

[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? 
{
    
}

[CyrusNajmabadi]

This thread is for championing the language feature,

A very big part of that is even determining if the feature should be done and whether or not alternative approaches would be preferable instead. This fork of the conversation is entirely about that.

[CyrusNajmabadi]

I could be wrong, but it feels like you have not used the existing Method Contracts implementation.

Not only have I used it, but I was on the c# team when we tried to actually use it realistically in production. We had to discontinue the idea for many problems (perf being a particular large one of those). :-)

If things have changed and perf is actually at all acceptable level that allows these systems to scale up to real world codebase sizes effectively, then that would make things more palatable. However, even in my last survey of the state of things (admittedly like 5 years ago), all the contract systems still had major issues here.

[Lexcess]

Not only have I used it, but I was on the c# team when we tried to actually use it realistically in production. We had to discontinue the idea for many problems (perf being a particular large one of those). :-)

Glad I added the caveat about being wrong then! Perf was definitely an issue which is why I would always advocate for a more refined scope of contract options (dropping things like invariants, perhaps only offering pre-conditions to start with etc...).

The reason I said that though, was that your contributions seemed to dismiss what people did find useful about contracts, rather than contribute on how to rework the concept into something that would meet the bar as a language feature. I think most here are realistic about why Method Contracts as it was would never make it.

At a high level I like the idea of describing complex constraints inline in code. Not scattered off in separate types. Not implied by various test suites. Directly in my code. Without contracts we tend to use repetitive inline guard clauses (if you are lucky) and tests, plus we obviously do not have the same guard metadata model for use in API definitions and enforcement.

Obviously, the original implementation had some other cool features (inference for example), but personally I do not consider much from the original implementation to be sacred in the process of getting the concept adopted as a language feature.

So, if I could steer you, it would be towards what would a performant and robust language feature for people who like the concept of contracts look like? As opposed to simply arguing if they should exist at all or be constrained by the flaws and overambition of previous implementations.

[acaly]

Trying to persuade the team some feature is good or important to you is useless. They have said above that they would like to let you wait for 15 years.

One example is the recent "file private" visibility, which is a feature similar to what had been proposed by community years ago, but is only discussed seriously recently when the c# runtime team found it useful.

[CyrusNajmabadi]

The reason I said that though, was that your contributions seemed to dismiss what people did find useful about contracts,

I def can appreciate what people find useful. But at the same time, making a language change means we have to have practical solutions here. :-)

[CyrusNajmabadi]

They have said above that they would like to let you wait for 15 years.

Right. I don't get what's contentious about that. If the feature takes 15 years until it's viable then we shouldn't be shipping earlier.

[CyrusNajmabadi]

but is only discussed seriously

This feature has been discussed seriously.

when the c# runtime team found it useful.

This is not the case. The discussion was advanced because a reasonable proposal was put forth that actually handled a whole host of concerns that are needed.

We have limited resources, so having a realistic proposal or forth that goes in depth and works to balance many concerns, addresses costs, and thinks about how it can be expanded in the future, ends up being something that here attention enough from an ldm member to champion.

[Clockwork-Muse]

The latter happens all the time. A lib adds a more restrictive check, but all the data that actually flows into it is fine. Now there is no break. Contrast this with a contract break where now you must actually unbreak things before you can actually proceed.

In context, I was speaking about a more restrictive check that would be triggered by an application constant. That is, the data that flowed in would never be fine, so the build would be broken regardless of whether it was due to a compile-time contract or the type's runtime check on application load.

It's one of the strong reasons we don't do things like encode exceptions into our ABI.

... I mean, I'd like checked exceptions too, if I could get them (But that would require quite a bit wider changes to the exception ecosystem, a la Midori).

[CyrusNajmabadi]

So, if I could steer you, it would be towards what would a performant and robust language feature for people who like the concept of contracts look like?

I genuinely don't know. I've seen many attempts at this that have not been viable. So my default position here is that efforts would likely be better allocated elsewhere.

I do think if someone in the community, or other venues (like academia) can prove this out, then that would certainly make things much more likely.

I personally have no clue how to pull this off. I wish I did! :-)

[CyrusNajmabadi]

so the build would be broken regardless of whether it was due to a compile-time contract or the type's runtime check on application load.

I think the challenge is more at the edges. Say one API says it generates values from the set S, and one API says it takes values from the same set. But then the second API changes to {S-1}. Now you have a contract break. However, it's entirely possible that in reality that single value that is not accepted is not actually ever generated by the first API (it's just marked that way as a reasonable, slightly broader, contract).

This would now break with a contract incongruity, despite very possibly not being an actual problem for these libs. That's why I don't want to actually encode this as an abi. I'd far prefer it as just a relaxed analysis system that layers on top.

This is also much more palatable as such analysis is not encumbered by the same compat rules we have. A different owner can decide a different set of rules and compat decisions that make sense to them.

[CyrusNajmabadi]

... I mean, I'd like checked exceptions too, if I could get them (But that would require quite a bit wider changes to the exception ecosystem, a la Midori).

I'd love to see a design there that can work in practice. For example how would a linq system work with checked exceptions? How do you support passing delegates to things when exceptions are part of your signatures?

[Clockwork-Muse]

This would now break with a contract incongruity, despite very possibly not being an actual problem for these libs. That's why I don't want to actually encode this as an abi. I'd far prefer it as just a relaxed analysis system that layers on top.

I don't think I really disagree with this concern.
What I'm wondering about here is whether we could get the runtime/JIT in on the act for stuff like this. That is, the ABI has the signatures, and at load/JIT time it compares them - if they're compatible it discards any checks, otherwise it emits the necessary checks to throw them as runtime errors. As a rough concept, this also allows it to work with libraries that haven't been compiled with the necessary information, since it would be considered as having no validation.

I'd love to see a design there that can work in practice. For example how would a linq system work with checked exceptions? How do you support passing delegates to things when exceptions are part of your signatures?

From the look of things, Midori would have done something like

public static class Enumerable 
{
    public static TResult Select<TSource, TResult, throws E>(this IEnumerable<TSource> source, Func<TSource, TResult, E> selector) E
    {
        foreach (TSource element in source)
        {
            yield return try selector(element);
        }
    }
}

// I don't think you needed to do anything at the call site if you couldn't throw a non-abandonment exception?  Blog slightly unclear here.
// Something like normal.
var n = new [] { 1, 2, 3 }.Select(n => n + 1);
var n = try new [] { 1, 2, 3 }.Select(n => throw new IOException());

... although probably IOException is the only exception that might be reasonably be needed to be used in such a situation - most of the others causing abandonment, and not meaning to be caught.

[MovGP0]

• Day can never be over 31
• Month must be between 1 and 12
• Second must be between 0 and 59 (in the case of TimeSpan, -59 and 59)
• etc.

I think you should check out this:

• Falsehoods programmers believe about time

Or for a more complete list:

• Awesome Falsehood

[Rekkonnect]

I think you should check out this:

• Falsehoods programmers believe about time

Yeah I was already told that time is far more disgusting than I thought. Not part of the discussion.

Part of the discussion now:

I genuinely don't know. I've seen many attempts at this that have not been viable. So my default position here is that efforts would likely be better allocated elsewhere.

Internal attempts in the C# team? Or general attempts like other languages (Dafny is one that comes to my mind).

I do think if someone in the community, or other venues (like academia) can prove this out, then that would certainly make things much more likely.

What kind of performance are we talking about? Compilation or runtime? Because compile-time contracts are what I have been dreaming of, eliminating runtime checks, further improving performance in the process, in alignment with runtime support and JIT optimizations.

[Lexcess]

The discussion was advanced because a reasonable proposal was put forth that actually handled a whole host of concerns that are needed.

I am not sure if I have seen this proposal, nor the remaining concerns that meant it didn't pass muster. Could you link or copy both here?

[acaly]

The discussion was advanced because a reasonable proposal was put forth that actually handled a whole host of concerns that are needed.

I am not sure if I have seen this proposal, nor the remaining concerns that meant it didn't pass muster. Could you link or copy both here?

Actually I don't think the proposal I was talking about ("file private" visibility, as I don't want to create a reference I would not provide a link here) can be considered "a reasonable proposal put forth" at the time most discussion happened. Most of the content was added later.

There are many examples in this repo that someone from the community wrote a much longer proposal and got no more than 2 replies. It is not a very good experience to spend time writing proposals here. As I said, it is very hard to persuade the team to do or not to do something. Such work is better left to themselves.

[Lexcess]

The discussion was advanced because a reasonable proposal.

Apologies, I misunderstood. From the reply I thought there was such a proposal for contracts.

[marinasundstrom]

I created a proposal for a compile-time Code Contracts based on attributes that can be analyzed as part of the development experience.

https://github.com/marinasundstrom/CodeContractsTest

The analyzer is not there. But I give hints on what kind of errors there could be.

There is also a syntax proposal.

I know that someone has already been experimenting with implementing it into the compiler.

[Genbox]

There is also a syntax proposal.

I personally like it. Just thinking about having IntelliSense and compile-time checking of the contract specs makes me all giddy.
I think both approaches should be implemented - that way the language extension could compile into the attribute, and an analyzer on the consumer's side could check the contract.

For example:

public int CalculateLevel(int userLevel)
    requires userLevel >= 0,
    ensures result >= 100
{
    int systemLevel = 100;
    return systemLevel + userLevel;
}

This would compile into a C# backward-compatible spec with attributes:

[Ensures("result >= 100")]
public int CalculateLevel([Requires(">=0")]int userLevel)
{
    int systemLevel = 100;
    return systemLevel + userLevel;
}

As such, an analyzer could easily traverse the AST, extract the attributes and run the SMT solver.

[marinasundstrom]

@Genbox Yes. This is the first step. Building the infrastructure.

There are a lot of advanced patterns to be dealt with (like str.Length < 10), but someone should at least try the simpler ones before ruling out its a bad idea.

An analyzer plugin can be written quite easily to test the concept. I did create a project for attempting that in my repo.

When it comes to the language syntax, I remember someone a long time ago (I think in this issue) posting a concept of implementing it in Roslyn.

From my repo:

// CS1234: Argument does not satisfy requirement: arg < 42
// CS1235: InvalidOperationException is unchecked.
var result = DoSomething(42);
                         ~~

// "result" is marked as satisfying > 0

// CS1234: Argument does not satisfy requirement: input < 0
Foo(result);
    ~~~~~~

[Throws(typeof(InvalidOperationException))]
[return: Ensures("return > 0")]
int DoSomething([Requires("arg >= 0"), Requires("arg < 42")] int arg)
{
    if(arg == 10)
    {
        throw new InvalidOperationException();
    }
    return arg;
}

void Foo([Requires("input < 0")] int input)
{

}

Another example:

File file = new ();

// "name" is satisying Length =< 50;
var name = file.FileName;

// This means that you get an error or warning

// CS1234: Argument does not satisfy requirement: fileName.Length >= 60
ReadFile(name);
         ~~~~

void ReadFile([Requires("fileName.Length >= 60")] string fileName)
{

}

class File 
{
    public string FileName 
    {
        [return: Ensures("return.Length =< 50")]
        get;
    } = null!;
}

[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: ***@***.***>