New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proposal: Method Contracts #119

Closed
stephentoub opened this Issue Jan 28, 2015 · 258 comments

Comments

@stephentoub
Member

stephentoub commented Jan 28, 2015

(Note: this proposal was briefly discussed in #98, the C# design notes for Jan 21, 2015. It has not been updated based on the discussion that's already occurred on that thread.)

Background

"Code Contracts" were introduced in .NET 4 as a feature of the Framework, primarily exposed through the System.Diagnostics.Contracts.Contract class. Through method calls like Contract.Requires and Contract.Ensures, developers could add code to their methods to specify preconditions and postconditions, and then a subsequent tool known as a rewriter could be used to post-process the code generated by the compiler to appropriately implement the expressed contracts, e.g. whereas the developer puts a call to Ensures at the beginning of the method, the rewriter ensures that path through the method that could cause it to exit ends with a validation of the expressed postcondition.

public int Insert(T item, int index)
{
    Contract.Requires(index >= 0 && index <= Count);
    Contract.Ensures(Contract.Result<int>() >= 0 && Contract.Result<int>() < Count);
    return InsertCore(item, index);
}

Problem

Very little code actually uses these API-based code contracts. They require additional tooling to be integrated into the build, they're verbose, and it's difficult to write additional robust tooling related to them (e.g. integrating contract information into documentation).

Solution: Language support for method contracts

Basic contract support for preconditions and postconditions can be built directly into the language, without requiring any separate tooling or custom build processes, and more thoroughly integrated throughout the language.

The compiler would generate all of the relevant code to correctly validate the contracts, and the contracts would show up as part of the method signature in the Visual Studio IDE, such as in IntelliSense at call sites to the method.

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

These contracts would primarily be validated at run time, however if the compiler (or a 3rd-party diagnostic) could statically detect a violated contract (e.g. a precondition requires that an argument be non-null, and null is being passed as the argument), it could choose to fail the compilation rather than allowing the bug to make its way to run time. Similarly, if the compiler (frontend or backend) is able to statically determine that a contract will always be satisfied, it can optimize based on that knowledge.

Unlike .NET Code Contracts, which have configurable but complicated behavior provided by a post-compilation rewriter tool (and which are no-ops if such a rewriter isn’t used), failed validation of ‘requires’ and ‘ensures’ clauses would ideally result in "fail fast" (ala Environment.FailFast(...)), meaning the program abandons immediately. This is very useful for validating preconditions and postconditions, which are typically used to catch usage errors by the developer. Such errors should never make it into production.

The compiler would require that preconditions and postconditions can be validated by the caller, and as such it requires that any members used in the requires and ensures clauses are all accessible to any caller, e.g. the requires clause of a public method may not access internal or private members, and the requires clause of an internal method may not access private members.

Preconditions and postconditions should also not throw exceptions.

Virtual methods and interface methods may have preconditions and postconditions, in which case the compiler guarantees that overrides and implementations of these methods satisfy the preconditions. To make this clear to a developer reading the code, the override or interface implementation would state "requires base" or "ensures base", to indicate that there are imposed constraints, while not forcing the developer writing the code to explicitly type them out.

interface IItemCollection
{
    int Count ensures return >= 0 { get; }
    …
}

class MyItemCollection : IItemCollection
{
    public int Count ensures base => m_count;
    …
}

Alternatives: Fail fast vs exceptions

In support of migrating existing code to use contracts, or for places where an exception is really desired over fail fast, we could optionally consider additional syntax to specify that an exception should be thrown instead of fail fasting.

For example, the previous Insert example's requires and ensures clauses would result in fail fasting if a condition isn't met:

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

But, the developer could explicitly override the fail fast by specifying what should happen in case of failure:

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

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Jan 28, 2015

Any possibility of getting invariants as well?

Would love to see the static analysis tools we have in Code Contracts working with these new contracts.

I really like the presented syntax to decide between exceptions and fail-fast for preconditions.

aarondandy commented Jan 28, 2015

Any possibility of getting invariants as well?

Would love to see the static analysis tools we have in Code Contracts working with these new contracts.

I really like the presented syntax to decide between exceptions and fail-fast for preconditions.

@aarondandy

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Jan 28, 2015

Could some kind of flag be provided to omit private/internal contracts from release builds if we have static analysis tools to prove them?

aarondandy commented Jan 28, 2015

Could some kind of flag be provided to omit private/internal contracts from release builds if we have static analysis tools to prove them?

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Jan 28, 2015

Member

@aarondandy

In previous research we have shied way from invariants in part because it's actually incredibly difficult for developers to predict the effect it will have on the code. Typically invariants checks are validated to be true on every exit / entry point of a given method. Given that can you point out all of the places on the following method where that happens?

class C
{
  invarint Count >= 0

  int[] _array;
  int _count;

  void AddRange(IEnumerable<int> all) 
  {
    EnsureCapacity();
    foreach (var cur in all) {
      _array[i] = cur;
    }
  }
}

Here are just a few of the places where an invariant check must occur in the above code:

  • In the generated call to GetEnumerator.
  • Twice per loop iteration. Once for MoveNext and Current each.
  • Before and after the call to EnsureCapacity
  • At least twice inside the implementation of EnsureCapacity
  • At the beginning and end of the method.

Sure a few of these may be able to be optimized away. But even then on this really simple method the invariant check is occurring at a very high frequency.

In the past when we looked deeply at places where developers wanted invariants we found that requires and ensures were sufficient to the task.

Member

jaredpar commented Jan 28, 2015

@aarondandy

In previous research we have shied way from invariants in part because it's actually incredibly difficult for developers to predict the effect it will have on the code. Typically invariants checks are validated to be true on every exit / entry point of a given method. Given that can you point out all of the places on the following method where that happens?

class C
{
  invarint Count >= 0

  int[] _array;
  int _count;

  void AddRange(IEnumerable<int> all) 
  {
    EnsureCapacity();
    foreach (var cur in all) {
      _array[i] = cur;
    }
  }
}

Here are just a few of the places where an invariant check must occur in the above code:

  • In the generated call to GetEnumerator.
  • Twice per loop iteration. Once for MoveNext and Current each.
  • Before and after the call to EnsureCapacity
  • At least twice inside the implementation of EnsureCapacity
  • At the beginning and end of the method.

Sure a few of these may be able to be optimized away. But even then on this really simple method the invariant check is occurring at a very high frequency.

In the past when we looked deeply at places where developers wanted invariants we found that requires and ensures were sufficient to the task.

@aarondandy

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Jan 28, 2015

@jaredpar

That is fair considering the complexity The real reason I want invariants is just to reduce the amount of redundant contracts I would need to write. As a compromise would it be terrible to have a way to reuse some pre/post conditions? Something like [ContractAbbreviator] but probably way different?

aarondandy commented Jan 28, 2015

@jaredpar

That is fair considering the complexity The real reason I want invariants is just to reduce the amount of redundant contracts I would need to write. As a compromise would it be terrible to have a way to reuse some pre/post conditions? Something like [ContractAbbreviator] but probably way different?

@theoy theoy added the Language-C# label Jan 28, 2015

@mirhagk

This comment has been minimized.

Show comment
Hide comment
@mirhagk

mirhagk Jan 28, 2015

@aarondandy Are you referring to reusing a pre-condition as a post-condition, or referring to reusing a precondition across several methods in a class?

For the first situation it'd be nice if requires ensures or some other syntactic sugar was supported. For the second, it could be handled with allowing the expression to be a method (which can be declared with the shorthand lambda method syntax), so you can have a CheckClassInvariants method and do requires ensures CheckClassInvariants() which isn't too bad.

mirhagk commented Jan 28, 2015

@aarondandy Are you referring to reusing a pre-condition as a post-condition, or referring to reusing a precondition across several methods in a class?

For the first situation it'd be nice if requires ensures or some other syntactic sugar was supported. For the second, it could be handled with allowing the expression to be a method (which can be declared with the shorthand lambda method syntax), so you can have a CheckClassInvariants method and do requires ensures CheckClassInvariants() which isn't too bad.

@aarondandy

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Jan 28, 2015

@mirhagk

"reusing a precondition across several methods" is what I meant but I like your other thoughts too. I don't really want to have a true provable invariant for Count >=0 but I definitely want a way to prove and communicate that each method call on my type won't do something crazy to Count.

aarondandy commented Jan 28, 2015

@mirhagk

"reusing a precondition across several methods" is what I meant but I like your other thoughts too. I don't really want to have a true provable invariant for Count >=0 but I definitely want a way to prove and communicate that each method call on my type won't do something crazy to Count.

@ejball

This comment has been minimized.

Show comment
Hide comment
@ejball

ejball Jan 28, 2015

I wonder if ensures could be made to work naturally with async method results.

ejball commented Jan 28, 2015

I wonder if ensures could be made to work naturally with async method results.

@alexpolozov

This comment has been minimized.

Show comment
Hide comment
@alexpolozov

alexpolozov Jan 28, 2015

Good to see that this is being considered!

Preconditions and postconditions should also not throw exceptions.

How are you going to verify this? For instance, are we allowed to do property access in contracts: requires id != this.Owner.Id? What if Owner is null? Is it an uncompilable code, a NullReferenceException at runtime, or a contract failure?

Just like in API-based Code Contracts, there should be some way to refer to the old (pre-invocation) value of the field/property/parameter. old(foo) looks good, but that makes old a new contextual keyword, which you don't like to introduce often.

alexpolozov commented Jan 28, 2015

Good to see that this is being considered!

Preconditions and postconditions should also not throw exceptions.

How are you going to verify this? For instance, are we allowed to do property access in contracts: requires id != this.Owner.Id? What if Owner is null? Is it an uncompilable code, a NullReferenceException at runtime, or a contract failure?

Just like in API-based Code Contracts, there should be some way to refer to the old (pre-invocation) value of the field/property/parameter. old(foo) looks good, but that makes old a new contextual keyword, which you don't like to introduce often.

@mirhagk

This comment has been minimized.

Show comment
Hide comment
@mirhagk

mirhagk Jan 28, 2015

@apskim

Preconditions and postconditions should also not throw exceptions.

This may or may not be enforced. It might just be a "you shouldn't do that" kind of thing rather than a compile time exception (perhaps static analyzers could look for it).

If it is a compile time thing, then regular property access would have to be disallowed in your case to instead do something like requires id <= this.Owner.?Id. This doesn't throw any exceptions and will fail the validation.

mirhagk commented Jan 28, 2015

@apskim

Preconditions and postconditions should also not throw exceptions.

This may or may not be enforced. It might just be a "you shouldn't do that" kind of thing rather than a compile time exception (perhaps static analyzers could look for it).

If it is a compile time thing, then regular property access would have to be disallowed in your case to instead do something like requires id <= this.Owner.?Id. This doesn't throw any exceptions and will fail the validation.

@drewnoakes

This comment has been minimized.

Show comment
Hide comment
@drewnoakes

drewnoakes Jan 28, 2015

Member

To what extent can the compiler check a type's contracts for internal consistency? For example, it'd be hard to reliably solve for arbitrary expressions:

class C
{
    double Value ensures Math.log10(return) > 0 { get; }

    void Foo() ensures Value < 1 { ... }
}

There is no value of x < 1 for which Math.log10(x) > 0.

Would these constraints primarily be evaluated at run-time, with best-effort use from tooling?


Also, if arbitrary code can be executed in requires and ensures statements, side effects must be considered. Code may behave differently when compiled to evaluate contracts vs. without.

Member

drewnoakes commented Jan 28, 2015

To what extent can the compiler check a type's contracts for internal consistency? For example, it'd be hard to reliably solve for arbitrary expressions:

class C
{
    double Value ensures Math.log10(return) > 0 { get; }

    void Foo() ensures Value < 1 { ... }
}

There is no value of x < 1 for which Math.log10(x) > 0.

Would these constraints primarily be evaluated at run-time, with best-effort use from tooling?


Also, if arbitrary code can be executed in requires and ensures statements, side effects must be considered. Code may behave differently when compiled to evaluate contracts vs. without.

@mirhagk

This comment has been minimized.

Show comment
Hide comment
@mirhagk

mirhagk Jan 28, 2015

@drewnoakes I'm assuming that an extension will be created that checks all sorts of crazy situations that you'd never want to add to a compiler (for complexity reasons). The compiler can do very minimum checks, and leave most of the checks to extensions.

In #98 it was mentioned that there may want to be some shorthand syntax for common checks (null being the most common). Something like requires item seems like a simple shorthand for the case of null checks, and combined with the ability to separate with a , would probably lead to a wider usage (requires item, data, index would be very simple to write and there'd be little reason to not use it).

An alternative is to use requires item! which makes use of the proposed non-nullable reference syntax ! and separates it from a boolean.

mirhagk commented Jan 28, 2015

@drewnoakes I'm assuming that an extension will be created that checks all sorts of crazy situations that you'd never want to add to a compiler (for complexity reasons). The compiler can do very minimum checks, and leave most of the checks to extensions.

In #98 it was mentioned that there may want to be some shorthand syntax for common checks (null being the most common). Something like requires item seems like a simple shorthand for the case of null checks, and combined with the ability to separate with a , would probably lead to a wider usage (requires item, data, index would be very simple to write and there'd be little reason to not use it).

An alternative is to use requires item! which makes use of the proposed non-nullable reference syntax ! and separates it from a boolean.

@Clockwork-Muse

This comment has been minimized.

Show comment
Hide comment
@Clockwork-Muse

Clockwork-Muse Jan 30, 2015

what about situations where a compile-time check is nice, but a runtime check may impart more of a performance penalty? For example, there's this comment in System.Collections.Immutable's array:

public T this[int index]
{
    get
    {
        // We intentionally do not check this.array != null, and throw NullReferenceException
        // if this is called while uninitialized.
        // The reason for this is perf.
        // Length and the indexer must be absolutely trivially implemented for the JIT optimization
        // of removing array bounds checking to work.
        return this.array[index];
    }
}

...which states that, while you want compile-time checks for existence of the array, and index range, the penalties for runtime checks are too high. (In this case they're letting the hardware/vm throw the errors directly, a rarer occurrence than checking all accesses)

Maybe the validator could biggyback off of hardware/vm protections? So it could see something like requires this.array, index >= 0 && index < this.array.Length, note that it has built-in runtime checks (effectively) for those values anyways, and noop them. Which would probably require sitting in the compiler, than as an external tool.

Clockwork-Muse commented Jan 30, 2015

what about situations where a compile-time check is nice, but a runtime check may impart more of a performance penalty? For example, there's this comment in System.Collections.Immutable's array:

public T this[int index]
{
    get
    {
        // We intentionally do not check this.array != null, and throw NullReferenceException
        // if this is called while uninitialized.
        // The reason for this is perf.
        // Length and the indexer must be absolutely trivially implemented for the JIT optimization
        // of removing array bounds checking to work.
        return this.array[index];
    }
}

...which states that, while you want compile-time checks for existence of the array, and index range, the penalties for runtime checks are too high. (In this case they're letting the hardware/vm throw the errors directly, a rarer occurrence than checking all accesses)

Maybe the validator could biggyback off of hardware/vm protections? So it could see something like requires this.array, index >= 0 && index < this.array.Length, note that it has built-in runtime checks (effectively) for those values anyways, and noop them. Which would probably require sitting in the compiler, than as an external tool.

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Jan 30, 2015

Member

@Clockwork-Muse

We've did pretty extensive profiling of contracts in our project and found that in general the performance hit they caused was minimal. It was usually in the 1-2% range across the system.

Sure there was the occasional check that was too expensive to make a contract. In those situations we first looked to the API itself. If verifying the invariants of the type was too expensive to put in a contract then perhaps the API itself needs to be changed.

If the API couldn't be made more efficient then we would move the check into Debug.Assert. That was pretty rare though (only a handful of occurrences).

Note: contracts do not always result in a negative performance hit. It is possible that they establish invariants (like bounds) that the JIT can optimize against and result in faster code. There were definitely places where that happened.

Member

jaredpar commented Jan 30, 2015

@Clockwork-Muse

We've did pretty extensive profiling of contracts in our project and found that in general the performance hit they caused was minimal. It was usually in the 1-2% range across the system.

Sure there was the occasional check that was too expensive to make a contract. In those situations we first looked to the API itself. If verifying the invariants of the type was too expensive to put in a contract then perhaps the API itself needs to be changed.

If the API couldn't be made more efficient then we would move the check into Debug.Assert. That was pretty rare though (only a handful of occurrences).

Note: contracts do not always result in a negative performance hit. It is possible that they establish invariants (like bounds) that the JIT can optimize against and result in faster code. There were definitely places where that happened.

@AdamSpeight2008

This comment has been minimized.

Show comment
Hide comment
@AdamSpeight2008

AdamSpeight2008 Jan 30, 2015

Contributor

Would it be possible to have a method contract in this position?

T Item(int index)
{
  requires (0 <= index) && (index < Size)
  get{ return _a[index]; }
  set(T item) { _a[index]=item; }
}

Using a trait ( #129)

T Item(int index)
{
  trait { _a!; range:  0 <= index < _a,Length; }
  get { _a[index]; }
  set(T item) { _a[index] = item; }
}
Contributor

AdamSpeight2008 commented Jan 30, 2015

Would it be possible to have a method contract in this position?

T Item(int index)
{
  requires (0 <= index) && (index < Size)
  get{ return _a[index]; }
  set(T item) { _a[index]=item; }
}

Using a trait ( #129)

T Item(int index)
{
  trait { _a!; range:  0 <= index < _a,Length; }
  get { _a[index]; }
  set(T item) { _a[index] = item; }
}
@brandf

This comment has been minimized.

Show comment
Hide comment
@brandf

brandf Jan 31, 2015

The part about Virtual methods and interface methods made me starting thinking about how this might be seen as an extension to the type system in a way...or rather another kind of type, similar to units of measure in F#. I'm bored, so I'm going to riff on the idea...

If we start with the first example in the solution above:

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

The 'requires' are additional constraints on the methods parameters, similar to how you have a types associated with each parameter. For fun I'm using 'where' below instead of adding new keywords. I think it's worth considering making it look LINQ'ish:

public int Insert(T item, int index where index >= 0 && index <= Count)
    where return >= 0 && return < Count
{
    return InsertCore(item, index);
}

Which then makes me think of the notion of generic type constraints. Similar to how a delegate gives a name to the shape of a function, a typeconstraint is used to give a name to a constraint.

typeconstraint Bounded<Type, Lower, Upper> = Type N where N >=0 Lower && N <= Upper

Perhaps you could then use typeconstraints anywhere you would normally use a type. The generic parameters could be bound to other types, constants, members or other arguments. Now the above can be rewritten:

public Bounded<int, 0, Count> Insert(T item, Bounded<int, 0, Count> index) 
{
    return InsertCore(item, index);
}

...which is looking pretty clean IMO.

And maybe I'm going off the deep end here, but lets consider going a step further by thinking of the traditional type syntax as being syntactic sugar for a specific where clause...

typeconstraint Bounded<T, Lower, Upper> n where typeof(n) is typeof(T) && n >= Lower && n <= Upper

In other words, 'traditional type syntax'...

int x

...is shorthand for...

var x where typeof(x) == typeof(int)

...or for parameters and returns...

x where typeof(x) == typeof(int)

Since non-nullable types are being considered at C#7 design meetings, lets see how that fits in with this:

typeconstraint NotNull n where n != null

...and union types (a bit like TypeScript has)

typeconstraint Union<T1, T2> n where typeof(n) == typeof(T1) || typeof(n) == typeof(T2)

And of course, similar to delegates, an assembly should be able to expose public typeconstraints like any other kind of type.

brandf commented Jan 31, 2015

The part about Virtual methods and interface methods made me starting thinking about how this might be seen as an extension to the type system in a way...or rather another kind of type, similar to units of measure in F#. I'm bored, so I'm going to riff on the idea...

If we start with the first example in the solution above:

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

The 'requires' are additional constraints on the methods parameters, similar to how you have a types associated with each parameter. For fun I'm using 'where' below instead of adding new keywords. I think it's worth considering making it look LINQ'ish:

public int Insert(T item, int index where index >= 0 && index <= Count)
    where return >= 0 && return < Count
{
    return InsertCore(item, index);
}

Which then makes me think of the notion of generic type constraints. Similar to how a delegate gives a name to the shape of a function, a typeconstraint is used to give a name to a constraint.

typeconstraint Bounded<Type, Lower, Upper> = Type N where N >=0 Lower && N <= Upper

Perhaps you could then use typeconstraints anywhere you would normally use a type. The generic parameters could be bound to other types, constants, members or other arguments. Now the above can be rewritten:

public Bounded<int, 0, Count> Insert(T item, Bounded<int, 0, Count> index) 
{
    return InsertCore(item, index);
}

...which is looking pretty clean IMO.

And maybe I'm going off the deep end here, but lets consider going a step further by thinking of the traditional type syntax as being syntactic sugar for a specific where clause...

typeconstraint Bounded<T, Lower, Upper> n where typeof(n) is typeof(T) && n >= Lower && n <= Upper

In other words, 'traditional type syntax'...

int x

...is shorthand for...

var x where typeof(x) == typeof(int)

...or for parameters and returns...

x where typeof(x) == typeof(int)

Since non-nullable types are being considered at C#7 design meetings, lets see how that fits in with this:

typeconstraint NotNull n where n != null

...and union types (a bit like TypeScript has)

typeconstraint Union<T1, T2> n where typeof(n) == typeof(T1) || typeof(n) == typeof(T2)

And of course, similar to delegates, an assembly should be able to expose public typeconstraints like any other kind of type.

@chrisaut

This comment has been minimized.

Show comment
Hide comment
@chrisaut

chrisaut Feb 4, 2015

I mentioned it in the original discussion, but what about a short hand syntax for the most common scenarios:

public void M(string! x) {}

expands to:

public void M(string x) requies x != null {}
public void M(int >= 0 x) {}

expands to:

public void M(int x) requires x >= 0 {}
public int >= 0 Count() {}

expands to:

public int Count() ensures return >= 0 {}
public void M(int < y x, int > x y) {}

expands to:

public void M(int x, int y) requires x < y, requires y > x {}

(this specific case looks messy, thus probably ok to only support short hand for simple cases, like operators and constant literals (no method calls, no refering to other arguments or fields/properties etc, for that you would use the "full" syntax).

public C! M(B! b) {}

expands to:

public C M(B b) requires m != null, ensures return != null

I think of contracts as a harder "type", thus I feel it might make sense to have the requirements right there with the parameter (it also avoids double typing).
For instance you don't say
public M(x) requires x is int, the int requirement is right there with the parameter, so why would further requirements on x not be right along there with it?

The downside is it might look a bit messy, especially if there are lots of parameters (but that's code smell anyways), and I guess it's (much?) harder to parse for the compiler.

chrisaut commented Feb 4, 2015

I mentioned it in the original discussion, but what about a short hand syntax for the most common scenarios:

public void M(string! x) {}

expands to:

public void M(string x) requies x != null {}
public void M(int >= 0 x) {}

expands to:

public void M(int x) requires x >= 0 {}
public int >= 0 Count() {}

expands to:

public int Count() ensures return >= 0 {}
public void M(int < y x, int > x y) {}

expands to:

public void M(int x, int y) requires x < y, requires y > x {}

(this specific case looks messy, thus probably ok to only support short hand for simple cases, like operators and constant literals (no method calls, no refering to other arguments or fields/properties etc, for that you would use the "full" syntax).

public C! M(B! b) {}

expands to:

public C M(B b) requires m != null, ensures return != null

I think of contracts as a harder "type", thus I feel it might make sense to have the requirements right there with the parameter (it also avoids double typing).
For instance you don't say
public M(x) requires x is int, the int requirement is right there with the parameter, so why would further requirements on x not be right along there with it?

The downside is it might look a bit messy, especially if there are lots of parameters (but that's code smell anyways), and I guess it's (much?) harder to parse for the compiler.

@AdamSpeight2008

This comment has been minimized.

Show comment
Hide comment
@AdamSpeight2008

AdamSpeight2008 Feb 4, 2015

Contributor

@chrisaut public void M(int < y x, int > x y) {} can never be satisfied

I think the ( #129 ) would be a better approach.

public void M(int x, int y)
  trait { x < y; y > x }
  {}

As it doesn't mess with the parameters syntax, yet still available for the IDE to use the user and collapse the trait definition.

Contributor

AdamSpeight2008 commented Feb 4, 2015

@chrisaut public void M(int < y x, int > x y) {} can never be satisfied

I think the ( #129 ) would be a better approach.

public void M(int x, int y)
  trait { x < y; y > x }
  {}

As it doesn't mess with the parameters syntax, yet still available for the IDE to use the user and collapse the trait definition.

@chrisaut

This comment has been minimized.

Show comment
Hide comment
@chrisaut

chrisaut Feb 4, 2015

@chrisaut public void M(int < y x, int > x y) {} can never be satisfied

why not?
it expands to:

public void M(int x, int y) requires x < y, requires y > x {}

x needs to be smaller than y, and y needs to be bigger than x (which comes from the first constraint, you wouldn't even need the second constraint).
M(0, 1) satisfies it.
But it just goes to show that for anything but trivial "< constant" stuff the syntax is confusing, hence it's probably not a good idea to allow it for anything that referes to other named parameters/fields/etc.

chrisaut commented Feb 4, 2015

@chrisaut public void M(int < y x, int > x y) {} can never be satisfied

why not?
it expands to:

public void M(int x, int y) requires x < y, requires y > x {}

x needs to be smaller than y, and y needs to be bigger than x (which comes from the first constraint, you wouldn't even need the second constraint).
M(0, 1) satisfies it.
But it just goes to show that for anything but trivial "< constant" stuff the syntax is confusing, hence it's probably not a good idea to allow it for anything that referes to other named parameters/fields/etc.

@AdamSpeight2008

This comment has been minimized.

Show comment
Hide comment
@AdamSpeight2008

AdamSpeight2008 Feb 4, 2015

Contributor

May have misread it as x < y and y < x

Contributor

AdamSpeight2008 commented Feb 4, 2015

May have misread it as x < y and y < x

@sirinath

This comment has been minimized.

Show comment
Hide comment
@sirinath

sirinath Feb 5, 2015

I don't see why this should be method only. Why not be able to use with variables also. In addition some distinction on runtime, compile time if unable at compile time at runtime and enforceability.

sirinath commented Feb 5, 2015

I don't see why this should be method only. Why not be able to use with variables also. In addition some distinction on runtime, compile time if unable at compile time at runtime and enforceability.

@AdamSpeight2008

This comment has been minimized.

Show comment
Hide comment
@AdamSpeight2008
Contributor

AdamSpeight2008 commented Feb 5, 2015

@vkhorikov

This comment has been minimized.

Show comment
Hide comment
@vkhorikov

vkhorikov Feb 6, 2015

@jaredpar consider binding this feature to non-nullable reference types.
Although they can't be implemented as they are implemented in, for example, F# but some kind of 'global precondition' can mitigate the problem: it can state that no reference type within a class can have null value.
This will help to reduce amount of '!= null' preconditions in code that tries to be more functional.

vkhorikov commented Feb 6, 2015

@jaredpar consider binding this feature to non-nullable reference types.
Although they can't be implemented as they are implemented in, for example, F# but some kind of 'global precondition' can mitigate the problem: it can state that no reference type within a class can have null value.
This will help to reduce amount of '!= null' preconditions in code that tries to be more functional.

@johncrim

This comment has been minimized.

Show comment
Hide comment
@johncrim

johncrim Feb 9, 2015

Could you explain why run-time contract violation shouldn't throw an exception? I've shied away from using CodeContracts static analysis (build are too slow; too much work to fix all warnings), but find them great for run-time validation and documentation. It's also great to be able to dial up and down the amount of run-time checks for debug and release builds (full checks vs ReleaseRequires). In the case of release builds, you DEFINITELY don't want fail-fast behavior; and arguably you'd want consistent behavior but more checks in debug builds.

My biggest problems with CodeContracts have been:

  1. The post-processing step slows down the build a HUGE amount (CodeContracts seems to account for 80% of the build time). This is the main reason I've considered dropping CodeContracts on several occasions.
  2. The syntax could be more readable/expressive/concise
  3. The implementation is completely broken on Mono - this is the primary reason why developers with Macs are having to run Windows VMs.

I would expect that this proposal would address 1 and 2 at a minimum, so I'm a huge fan.

Another important trait to preserve is the ability to intercept contract failures and customize the response: log them, pop up a dialog, etc.

johncrim commented Feb 9, 2015

Could you explain why run-time contract violation shouldn't throw an exception? I've shied away from using CodeContracts static analysis (build are too slow; too much work to fix all warnings), but find them great for run-time validation and documentation. It's also great to be able to dial up and down the amount of run-time checks for debug and release builds (full checks vs ReleaseRequires). In the case of release builds, you DEFINITELY don't want fail-fast behavior; and arguably you'd want consistent behavior but more checks in debug builds.

My biggest problems with CodeContracts have been:

  1. The post-processing step slows down the build a HUGE amount (CodeContracts seems to account for 80% of the build time). This is the main reason I've considered dropping CodeContracts on several occasions.
  2. The syntax could be more readable/expressive/concise
  3. The implementation is completely broken on Mono - this is the primary reason why developers with Macs are having to run Windows VMs.

I would expect that this proposal would address 1 and 2 at a minimum, so I'm a huge fan.

Another important trait to preserve is the ability to intercept contract failures and customize the response: log them, pop up a dialog, etc.

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Feb 9, 2015

Member

@johncrim

Could you explain why run-time contract violation shouldn't throw an exception?

Contract violations occur when code has called into a method and provided invalid arguments or when the type itself was in an invalid state. This represents a coding error in the calling code. It simply failed to meet the basic contract of the method in question.

The safest thing to do in the face of a coding error is to stop executing code. The program is in an undefined state and continuing to execute code could lead to all manner of issues including: data corruption, later errors which mask the original bug, etc ...

This is why contract violations use Environment.FailFast (or the like) in the event of a failure. It ensures the process will be torn down in the most expedient manner possible. Crash dumps will point directly at the bug in question. Throwing an exception is instead a way to guarantee that user code will continue executing the program in an undefined state.

Member

jaredpar commented Feb 9, 2015

@johncrim

Could you explain why run-time contract violation shouldn't throw an exception?

Contract violations occur when code has called into a method and provided invalid arguments or when the type itself was in an invalid state. This represents a coding error in the calling code. It simply failed to meet the basic contract of the method in question.

The safest thing to do in the face of a coding error is to stop executing code. The program is in an undefined state and continuing to execute code could lead to all manner of issues including: data corruption, later errors which mask the original bug, etc ...

This is why contract violations use Environment.FailFast (or the like) in the event of a failure. It ensures the process will be torn down in the most expedient manner possible. Crash dumps will point directly at the bug in question. Throwing an exception is instead a way to guarantee that user code will continue executing the program in an undefined state.

@ulrichb

This comment has been minimized.

Show comment
Hide comment
@ulrichb

ulrichb Feb 9, 2015

I totally agree that in theory a developer's / coding error in the calling code should immediately stop the program.

But: Are we sure that in practice there are no legitimate use cases where we want to fail into a safe state in an exception handler (i.e. log errors using existing infrastructure; send error replies in a distributed system; ...) even in case of developer errors i.e. contract violations at run-time?

ulrichb commented Feb 9, 2015

I totally agree that in theory a developer's / coding error in the calling code should immediately stop the program.

But: Are we sure that in practice there are no legitimate use cases where we want to fail into a safe state in an exception handler (i.e. log errors using existing infrastructure; send error replies in a distributed system; ...) even in case of developer errors i.e. contract violations at run-time?

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Feb 10, 2015

Member

@ulrichb

Sure but in those case I would say that exceptions are a better choice than contracts. In my mind I view the difference between exceptions and contracts as follows:

  • Contracts: a precondition than can easily and efficiently be tested / guaranteed by the caller. If this precondition is violated then it clearly indicates a bug in the program.
  • Exceptions: used when a situation where a precondition can't efficiently, conveniently or simply can't be tested / guaranteed by the caller. Greatest example here is IO (it can always fail).
Member

jaredpar commented Feb 10, 2015

@ulrichb

Sure but in those case I would say that exceptions are a better choice than contracts. In my mind I view the difference between exceptions and contracts as follows:

  • Contracts: a precondition than can easily and efficiently be tested / guaranteed by the caller. If this precondition is violated then it clearly indicates a bug in the program.
  • Exceptions: used when a situation where a precondition can't efficiently, conveniently or simply can't be tested / guaranteed by the caller. Greatest example here is IO (it can always fail).
@ulrichb

This comment has been minimized.

Show comment
Hide comment
@ulrichb

ulrichb Feb 10, 2015

@jaredpar

What I meant was, that even in the case that we have a contract violation due to a developer error / bug in the program, do we always want to FailFast()?

One example: If we implement an HTTP server and request input leads to a precondition violation (due to a bug in the program), do we want to crash the whole server application (including all other request threads)? I think we should have the possibility that the contract violation throws an exception, i.e. just aborts the current request, and logs the contract violation, like it would happen with thrown NullReferenceExceptions (which are also bugs).

ulrichb commented Feb 10, 2015

@jaredpar

What I meant was, that even in the case that we have a contract violation due to a developer error / bug in the program, do we always want to FailFast()?

One example: If we implement an HTTP server and request input leads to a precondition violation (due to a bug in the program), do we want to crash the whole server application (including all other request threads)? I think we should have the possibility that the contract violation throws an exception, i.e. just aborts the current request, and logs the contract violation, like it would happen with thrown NullReferenceExceptions (which are also bugs).

@aarondandy

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Feb 10, 2015

@jaredpar

I could understand that view if static analysis tools were forced to run for everybody. Currently with the Code Contracts implementation I think it is rare for a user of a library to actually run static analysis against their project. Even if it was baked into the compiler I would think that especially during day-to-day development activities some people would want to temporarily disable static analysis if they are building and testing frequently. That is how I work anyway. In these cases it is pretty nice if I just get an ArgumentNull exception that I can see in my test and say "oops!"

I do still agree with "contract violation shouldn't throw an exception" but for a totally different reason I think. I like to see it kind of like driving with a sharp spike on your steering wheel, you would hopefully take extra care to not rear-end anybody. I find that when I am more likely to get an exception (or any failure really) due to violating a contract I am less likely to violate the contract as it makes me more careful. Static analysis tools help a bunch as well in that area.

aarondandy commented Feb 10, 2015

@jaredpar

I could understand that view if static analysis tools were forced to run for everybody. Currently with the Code Contracts implementation I think it is rare for a user of a library to actually run static analysis against their project. Even if it was baked into the compiler I would think that especially during day-to-day development activities some people would want to temporarily disable static analysis if they are building and testing frequently. That is how I work anyway. In these cases it is pretty nice if I just get an ArgumentNull exception that I can see in my test and say "oops!"

I do still agree with "contract violation shouldn't throw an exception" but for a totally different reason I think. I like to see it kind of like driving with a sharp spike on your steering wheel, you would hopefully take extra care to not rear-end anybody. I find that when I am more likely to get an exception (or any failure really) due to violating a contract I am less likely to violate the contract as it makes me more careful. Static analysis tools help a bunch as well in that area.

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Feb 10, 2015

Member

@ulrichb

One example: If we implement an HTTP server and request input leads to a precondition violation (due to a bug in the program), do we want to crash the whole server application (including all other request threads)?

This is confusing user input validation with method argument validation.

User input should never be done with a contract because as you pointed out it shouldn't be a tool to crash the process. That type of sanitation should be a separate process.

Member

jaredpar commented Feb 10, 2015

@ulrichb

One example: If we implement an HTTP server and request input leads to a precondition violation (due to a bug in the program), do we want to crash the whole server application (including all other request threads)?

This is confusing user input validation with method argument validation.

User input should never be done with a contract because as you pointed out it shouldn't be a tool to crash the process. That type of sanitation should be a separate process.

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Feb 10, 2015

Member

@aarondandy

I think it is rare for a user of a library to actually run static analysis against their project. Even if it was baked into the compiler I would think that especially during day-to-day development activities some people would want to temporarily disable static analysis if they are building and testing frequently

I do want to be clear that the compiler won't be doing any static analysis on the contracts the users supplies. These are simply a tool for argument validation.

That being said the output of contracts is expressive enough that theorem provers can run over the code.

Member

jaredpar commented Feb 10, 2015

@aarondandy

I think it is rare for a user of a library to actually run static analysis against their project. Even if it was baked into the compiler I would think that especially during day-to-day development activities some people would want to temporarily disable static analysis if they are building and testing frequently

I do want to be clear that the compiler won't be doing any static analysis on the contracts the users supplies. These are simply a tool for argument validation.

That being said the output of contracts is expressive enough that theorem provers can run over the code.

@ulrichb

This comment has been minimized.

Show comment
Hide comment
@ulrichb

ulrichb Feb 10, 2015

@jaredpar

... leads to a precondition violation (due to a bug in the program) ...

ulrichb commented Feb 10, 2015

@jaredpar

... leads to a precondition violation (due to a bug in the program) ...

@jaredpar

This comment has been minimized.

Show comment
Hide comment
@jaredpar

jaredpar Feb 10, 2015

Member

@ulrichb

How is that inconsistent with my argument?

Member

jaredpar commented Feb 10, 2015

@ulrichb

How is that inconsistent with my argument?

@aarondandy

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Feb 10, 2015

@jaredpar I may have misunderstood your previous comments, so ignore if so. The point I am making is that if FastFail is the only way that contracts are enforced I think it would be vary inconvenient for users of those methods. I think that having a choice between a contract throwing an exception or doing fastfail is important.

aarondandy commented Feb 10, 2015

@jaredpar I may have misunderstood your previous comments, so ignore if so. The point I am making is that if FastFail is the only way that contracts are enforced I think it would be vary inconvenient for users of those methods. I think that having a choice between a contract throwing an exception or doing fastfail is important.

@mcetkovsky

This comment has been minimized.

Show comment
Hide comment
@mcetkovsky

mcetkovsky Aug 26, 2016

Mads Torgersen - MSFT at https://blogs.msdn.microsoft.com/dotnet/2016/08/24/whats-new-in-csharp-7-0/

Nothing on design by contract this time around, and I’m not sure if there will be anytime soon. We’ve looked a lot at contract-style features, and they tend to get quite verbose and complicated. I am not sure that they would carry their weight in added value as language features. But maybe, one day, if we can get the design right.
While people do use CodeContracts for many things, the 90% case seems to be dealing with null. We are eager to tackle the language integration of that in a more type-system-oriented way, allowing you to distinguish between nullable and nonnullable reference types and track correct usage based on that. I hope this can happen in the next major release of C#.

mcetkovsky commented Aug 26, 2016

Mads Torgersen - MSFT at https://blogs.msdn.microsoft.com/dotnet/2016/08/24/whats-new-in-csharp-7-0/

Nothing on design by contract this time around, and I’m not sure if there will be anytime soon. We’ve looked a lot at contract-style features, and they tend to get quite verbose and complicated. I am not sure that they would carry their weight in added value as language features. But maybe, one day, if we can get the design right.
While people do use CodeContracts for many things, the 90% case seems to be dealing with null. We are eager to tackle the language integration of that in a more type-system-oriented way, allowing you to distinguish between nullable and nonnullable reference types and track correct usage based on that. I hope this can happen in the next major release of C#.

@eyalsk

This comment has been minimized.

Show comment
Hide comment
@eyalsk

eyalsk Aug 27, 2016

@mcetkovsky Thank you for that, range checks are also valuable so it's not only null checks but they are right in that DbC tend to be verbose and complicate things.

Maybe someone can narrow the use-cases and come up with a better solution.

eyalsk commented Aug 27, 2016

@mcetkovsky Thank you for that, range checks are also valuable so it's not only null checks but they are right in that DbC tend to be verbose and complicate things.

Maybe someone can narrow the use-cases and come up with a better solution.

@asvishnyakov

This comment has been minimized.

Show comment
Hide comment
@asvishnyakov

asvishnyakov Aug 27, 2016

Contributor

We just need extension support by compiler. Then Code Contracts team will apply language extension step-by-step and after their work will complete, Roslyn team will may start discussion about including that code to compiler.

Contributor

asvishnyakov commented Aug 27, 2016

We just need extension support by compiler. Then Code Contracts team will apply language extension step-by-step and after their work will complete, Roslyn team will may start discussion about including that code to compiler.

@SunnyWar

This comment has been minimized.

Show comment
Hide comment
@SunnyWar

SunnyWar Sep 15, 2016

I lend my I support the final solution Midori came up with:

Joe Duffy said about contracts in Midori:

We ended up with a single kind of contract: one that was part of an API’s signature and checked all the time. If a compiler could prove the contract was satisfied at compile-time – something ... it was free to elide the check altogether. But code was guaranteed it would never execute if its preconditions weren’t satisfied. For cases where you wanted conditional checks, you always had the assertion system...

SunnyWar commented Sep 15, 2016

I lend my I support the final solution Midori came up with:

Joe Duffy said about contracts in Midori:

We ended up with a single kind of contract: one that was part of an API’s signature and checked all the time. If a compiler could prove the contract was satisfied at compile-time – something ... it was free to elide the check altogether. But code was guaranteed it would never execute if its preconditions weren’t satisfied. For cases where you wanted conditional checks, you always had the assertion system...

@jamesqo

This comment has been minimized.

Show comment
Hide comment
@jamesqo

jamesqo Oct 8, 2016

Contributor

Perhaps we could introduce a syntax for the developer to indicate that he/she wants the checks to be debug-only? For example, prefixing with @:

int NextPowerOfTwo(int value) @requires value < 0
{
}

This particular example would kind of line up with how you prefix commands with @ in Batch scripting and Makefiles to 'quiet' the normal echo you get from the command. (Although C# is a very different language from both of those.)

Alternatively, we could introduce an attribute such as [DebugOnlyContract], but that would take away much of the convenience of using this feature for debug checks I guess.

Contributor

jamesqo commented Oct 8, 2016

Perhaps we could introduce a syntax for the developer to indicate that he/she wants the checks to be debug-only? For example, prefixing with @:

int NextPowerOfTwo(int value) @requires value < 0
{
}

This particular example would kind of line up with how you prefix commands with @ in Batch scripting and Makefiles to 'quiet' the normal echo you get from the command. (Although C# is a very different language from both of those.)

Alternatively, we could introduce an attribute such as [DebugOnlyContract], but that would take away much of the convenience of using this feature for debug checks I guess.

@kruncher

This comment has been minimized.

Show comment
Hide comment
@kruncher

kruncher Oct 8, 2016

I would personally prefer the more verbose (but readable!) attribute over the obscure syntax.

kruncher commented Oct 8, 2016

I would personally prefer the more verbose (but readable!) attribute over the obscure syntax.

@jamesqo

This comment has been minimized.

Show comment
Hide comment
@jamesqo

jamesqo Oct 8, 2016

Contributor

@kruncher The meaning would be clear after the first time you learn what it means, so that would only be an issue for newcomers.

I guess another option though would be to simply have a debug contextual keyword like this:

int NextPowerOfTwo(int value) debug requires value > 0
{
}

Would be less typing than adding an attribute, and admittedly more readable than the @ syntax for newcomers, but it would require an extra few keystrokes.

Contributor

jamesqo commented Oct 8, 2016

@kruncher The meaning would be clear after the first time you learn what it means, so that would only be an issue for newcomers.

I guess another option though would be to simply have a debug contextual keyword like this:

int NextPowerOfTwo(int value) debug requires value > 0
{
}

Would be less typing than adding an attribute, and admittedly more readable than the @ syntax for newcomers, but it would require an extra few keystrokes.

@kruncher

This comment has been minimized.

Show comment
Hide comment
@kruncher

kruncher Oct 8, 2016

What is the advantage in having a debug only contract; surely a contract is a contract?

kruncher commented Oct 8, 2016

What is the advantage in having a debug only contract; surely a contract is a contract?

@jamesqo

This comment has been minimized.

Show comment
Hide comment
@jamesqo

jamesqo Oct 8, 2016

Contributor

@kruncher We may not want extra checks we know are true in performance-sensitive code. For example, it may prevent the JIT compiler from inlining a particular method. For example if you go to corefx where the BCL lives, you'll see that basically all of the checks of the internal/private methods are Debug.Asserts.

Contributor

jamesqo commented Oct 8, 2016

@kruncher We may not want extra checks we know are true in performance-sensitive code. For example, it may prevent the JIT compiler from inlining a particular method. For example if you go to corefx where the BCL lives, you'll see that basically all of the checks of the internal/private methods are Debug.Asserts.

@kruncher

This comment has been minimized.

Show comment
Hide comment
@kruncher

kruncher Oct 8, 2016

Hmmm, would it be useful to have a build option to simply disable all contracts for internal/private methods (i.e. an option that can be configured on/off for 'Debug', 'Release' or 'Custom')?

kruncher commented Oct 8, 2016

Hmmm, would it be useful to have a build option to simply disable all contracts for internal/private methods (i.e. an option that can be configured on/off for 'Debug', 'Release' or 'Custom')?

@jamesqo

This comment has been minimized.

Show comment
Hide comment
@jamesqo

jamesqo Oct 8, 2016

Contributor

@kruncher Hmm... might be a good idea, actually. A problem though is that you might want to enable the contracts for only certain internal/private methods.

Contributor

jamesqo commented Oct 8, 2016

@kruncher Hmm... might be a good idea, actually. A problem though is that you might want to enable the contracts for only certain internal/private methods.

@Lexcess

This comment has been minimized.

Show comment
Hide comment
@Lexcess

Lexcess Oct 10, 2016

In the Code Contracts implementation there is a explicit option for only checking 'public surface contracts' which exhibits this behaviour. The clear win here is that if a contract is asserted on private methods the Code Contracts implementation will require another assertion or assumption it on any callee meaning that if all callees have already validated the input you don't take the perf hit on checking again.

I'd say this behaviour is the same (or a slight subset of) the statement: "If a compiler could prove the contract was satisfied at compile-time – something ... it was free to elide the check altogether" from earlier in this thread.

Lexcess commented Oct 10, 2016

In the Code Contracts implementation there is a explicit option for only checking 'public surface contracts' which exhibits this behaviour. The clear win here is that if a contract is asserted on private methods the Code Contracts implementation will require another assertion or assumption it on any callee meaning that if all callees have already validated the input you don't take the perf hit on checking again.

I'd say this behaviour is the same (or a slight subset of) the statement: "If a compiler could prove the contract was satisfied at compile-time – something ... it was free to elide the check altogether" from earlier in this thread.

@jamesqo

This comment has been minimized.

Show comment
Hide comment
@jamesqo

jamesqo Oct 10, 2016

Contributor

@Lexcess

meaning that if all callees have already validated the input you don't take the perf hit on checking again.

Would not always work. For example, consider this code sample:

T Single<T>(IList<T> list)
{
    if (list == null || list.Count != 1) throw something;

    return SingleInternal(list);
}

T SingleInternal<T>(IList<T> list)
{
    Debug.Assert(list != null && list.Count == 1);

    return list[0];
}

A bad implementation of IList<T> could return different values of Count for the 2 invocations, even though it was not actually modified. So the compiler could not prove that the list.Count == 1 constraint would be satisfied, and would have to check the Count twice.

Contributor

jamesqo commented Oct 10, 2016

@Lexcess

meaning that if all callees have already validated the input you don't take the perf hit on checking again.

Would not always work. For example, consider this code sample:

T Single<T>(IList<T> list)
{
    if (list == null || list.Count != 1) throw something;

    return SingleInternal(list);
}

T SingleInternal<T>(IList<T> list)
{
    Debug.Assert(list != null && list.Count == 1);

    return list[0];
}

A bad implementation of IList<T> could return different values of Count for the 2 invocations, even though it was not actually modified. So the compiler could not prove that the list.Count == 1 constraint would be satisfied, and would have to check the Count twice.

@Lexcess

This comment has been minimized.

Show comment
Hide comment
@Lexcess

Lexcess Oct 10, 2016

I see what you are saying but I think it is a separate point. I think the point that you could have untrustworthy implementations (note that the MS Code Contracts has contracts for interfaces like IList so you could solve this) is different from needlessly reapplying the same checks all the way down a call stack.

It'd be interesting to see what the Code Contracts does around non-predictable return types such as your example and arbitrary yield returns. I've often found it's analyser was quite good at unravelling such problems.

Lexcess commented Oct 10, 2016

I see what you are saying but I think it is a separate point. I think the point that you could have untrustworthy implementations (note that the MS Code Contracts has contracts for interfaces like IList so you could solve this) is different from needlessly reapplying the same checks all the way down a call stack.

It'd be interesting to see what the Code Contracts does around non-predictable return types such as your example and arbitrary yield returns. I've often found it's analyser was quite good at unravelling such problems.

@aarondandy

This comment has been minimized.

Show comment
Hide comment
@aarondandy

aarondandy Oct 12, 2016

For that example Code Contracts seems to take the "if it hurts don't do that strategy" and assumes you are not trying to intentionally harm the stability of your system. It does this by requiring methods used in a contract to be [Pure] but it does not enforce that the method or property is actually "Pure".

aarondandy commented Oct 12, 2016

For that example Code Contracts seems to take the "if it hurts don't do that strategy" and assumes you are not trying to intentionally harm the stability of your system. It does this by requiring methods used in a contract to be [Pure] but it does not enforce that the method or property is actually "Pure".

@gafter

This comment has been minimized.

Show comment
Hide comment
@gafter

gafter Mar 28, 2017

Member

This is now tracked at dotnet/csharplang#105

Member

gafter commented Mar 28, 2017

This is now tracked at dotnet/csharplang#105

@MohammadHamdyGhanem

This comment has been minimized.

Show comment
Hide comment
@MohammadHamdyGhanem

MohammadHamdyGhanem Dec 18, 2017

as I explained in dotnet/csharplang#1198, this syntax will be shorter:

public <0,Count>int Insert(T item, <0,Count>int index)   {
    return InsertCore(item, index);
}

MohammadHamdyGhanem commented Dec 18, 2017

as I explained in dotnet/csharplang#1198, this syntax will be shorter:

public <0,Count>int Insert(T item, <0,Count>int index)   {
    return InsertCore(item, index);
}
@HaloFour

This comment has been minimized.

Show comment
Hide comment
@HaloFour

HaloFour Dec 18, 2017

@MohammadHamdyGhanem

It's also not particular generic. What if you wanted to convey a constraint that doesn't involve ranges?

HaloFour commented Dec 18, 2017

@MohammadHamdyGhanem

It's also not particular generic. What if you wanted to convey a constraint that doesn't involve ranges?

@yaakov-h

This comment has been minimized.

Show comment
Hide comment
@yaakov-h

yaakov-h Dec 18, 2017

Or even within ranges, disjointed ranges?

e.g. value must be between 0 and 100, or between 200 and 300.

yaakov-h commented Dec 18, 2017

Or even within ranges, disjointed ranges?

e.g. value must be between 0 and 100, or between 200 and 300.

@MohammadHamdyGhanem

This comment has been minimized.

Show comment
Hide comment
@MohammadHamdyGhanem

MohammadHamdyGhanem Dec 18, 2017

What you ask about is a complex condition already, and regular If statements can do it better.
If you want to complicat things, I suggest to use regular expression syntax such as:
[reg exp]int x;
This can allow writting constrains on string data types as well.
If we think at the Data Type level, any thing is poossible!
Thanks.

MohammadHamdyGhanem commented Dec 18, 2017

What you ask about is a complex condition already, and regular If statements can do it better.
If you want to complicat things, I suggest to use regular expression syntax such as:
[reg exp]int x;
This can allow writting constrains on string data types as well.
If we think at the Data Type level, any thing is poossible!
Thanks.

@yaakov-h

This comment has been minimized.

Show comment
Hide comment
@yaakov-h

yaakov-h Dec 18, 2017

@MohammadHamdyGhanem If statements only give you runtime checks, not compile-time safety.

yaakov-h commented Dec 18, 2017

@MohammadHamdyGhanem If statements only give you runtime checks, not compile-time safety.

@MohammadHamdyGhanem

This comment has been minimized.

Show comment
Hide comment
@MohammadHamdyGhanem

MohammadHamdyGhanem Dec 18, 2017

@yaakov-h
So what? This ia already the case with any assignment that evaluates in run-time.
int i = x/somefunction();
is not runtime safe.
We csn handle exceptions easily , but business logic errors will pass undetected unless writing extra validation code, which we do more often.
In data binding, if a value raises an exception, the bound control will reject it automatically preventing the user from entering bad values without writing extra code.

MohammadHamdyGhanem commented Dec 18, 2017

@yaakov-h
So what? This ia already the case with any assignment that evaluates in run-time.
int i = x/somefunction();
is not runtime safe.
We csn handle exceptions easily , but business logic errors will pass undetected unless writing extra validation code, which we do more often.
In data binding, if a value raises an exception, the bound control will reject it automatically preventing the user from entering bad values without writing extra code.

@MohammadHamdyGhanem

This comment has been minimized.

Show comment
Hide comment
@MohammadHamdyGhanem

MohammadHamdyGhanem Dec 18, 2017

Also: Method Contracts are not run time safe, and will raise exceptions. This is why we use try catch.

MohammadHamdyGhanem commented Dec 18, 2017

Also: Method Contracts are not run time safe, and will raise exceptions. This is why we use try catch.

@MohammadHamdyGhanem

This comment has been minimized.

Show comment
Hide comment
@MohammadHamdyGhanem

MohammadHamdyGhanem Dec 18, 2017

So, there are 4 possible ways to do it:

  1. Method contracts. It is verbose but can write generic conditions.
  2. Constrained Data Types: It is a compact syntax and can be extended to use regular expressions.
  3. Validation attributes: Like those used in ASP.NET MVC. It has no effect on the c# syntax if self, and we can use parameters that indicate the error message or other actions. But using attribute for individual method parameters and return value can make the code long and ugly!
  4. Writing an analyzer, which I cannot exactly understand !

Sure we all want some syntax to simplify validation codes.
We can make compromises. For example:
If the constrained types can cause problems, they can only be used to define properties and methods (parameters and return values). They are nit true types but just syntax annotations to tell compiler how validate values, so the compiler can convert then to contracts under the hood.
Attributes also can be used with properties and methods to supply error message and additional options to tell the compiler what to do when the data are not valid.
This approach says that contracts can still be used in more complicated situations (but I see that it is easer to use regular code statements)

MohammadHamdyGhanem commented Dec 18, 2017

So, there are 4 possible ways to do it:

  1. Method contracts. It is verbose but can write generic conditions.
  2. Constrained Data Types: It is a compact syntax and can be extended to use regular expressions.
  3. Validation attributes: Like those used in ASP.NET MVC. It has no effect on the c# syntax if self, and we can use parameters that indicate the error message or other actions. But using attribute for individual method parameters and return value can make the code long and ugly!
  4. Writing an analyzer, which I cannot exactly understand !

Sure we all want some syntax to simplify validation codes.
We can make compromises. For example:
If the constrained types can cause problems, they can only be used to define properties and methods (parameters and return values). They are nit true types but just syntax annotations to tell compiler how validate values, so the compiler can convert then to contracts under the hood.
Attributes also can be used with properties and methods to supply error message and additional options to tell the compiler what to do when the data are not valid.
This approach says that contracts can still be used in more complicated situations (but I see that it is easer to use regular code statements)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment