This project is read-only.

Code Contracts

Topics: C# Language Design
Aug 11, 2014 at 7:45 PM
Hi,

Are there any plans to add Code Contract keywords to C#? (Previously Spec#, I think.)

I'd really love to have this feature ASAP, especially for interfaces and abstract classes since the current design requires defining so-called "contract classes" that are a quite awkward, though necessary.

Very simple example:
public interface IDoThings
{
  void DoSomething(int x, int y)
    requires x >= 0
    requires x < y

  Foo DoSomethingElse(Baz o)
    requires o != null
    ensures result != null
    ensures result.Baz == o
}
Installing the external Code Contracts rewriter would still be required to have the runtime and static analysis benefits. But at the very least, supporting contract keywords in C# would allow Roslyn to expose important additional metadata to tools and extensions, which of course the Code Contracts tools themselves could use.

Furthermore, proposals such as record classes and primary constructors would also benefit greatly from this since as it stands there doesn't appear to be any way of doing argument validation at all.

Local functions were proposed and rejected though one of the cited benefits would have been iterator block argument validation without having to define a private method that calls into the iterator. It's great, but its usage would have been ugly. Alternatively, Code Contract keywords would signal unambiguously to the compiler that an expression's sole purpose is to validate conditions and thus it should remain in the defined method, while the compiler generates a hidden method for the iterator's body, called by the former.
public IEnumerable<int> Range(int count)
  requires count >= 0
{
  for (var i = 0; i < count; i++)
  {
    yield return i;
  }
}
becomes
public IEnumerable<int> Range(int count)
{
  Contract.Requires(count >= 0);
  Contract.Ensures(Contract.Result<IEnumerable<int>>() != null);

  return $Range(count);
}

private IEnumerable<int> $Range(int count)
{
  for (var i = 0; i < count; i++)
  {
    yield return i;
  }
}
Thanks,
Dave
Aug 12, 2014 at 1:15 AM
Edited Aug 12, 2014 at 1:18 AM
The code contracts code generation is a Code Contracts-specific library. How would C# implement this?

Why don't you just use Code Contracts if that's what you want?
Aug 12, 2014 at 1:45 AM
Hi,

I do use Code Contracts. Do you? :) If you do, then you know how unwieldy it is to workaround some of the "limitations" in the C# language. I described a few of those workarounds in the Code Contracts API; namely, interfaces and abstract classes. The proposed Record types is going to be yet another.

There are many more reasons for integrating Code Contract keywords into the language. When I get some more time I'll enumerate them.

Thanks,
Dave
Aug 12, 2014 at 2:01 AM
Hi,

Just to be clear, as mentioned previously I wasn't necessarily suggesting that the C# compiler actually include the API calls itself. The CC rewriter can do that should a dev choose to use it. The benefits without rewriting would be in compiler exposing contract metadata.

- Dave
Aug 12, 2014 at 2:06 AM
Hi,

Thinking about the concept some more, it's very similar to documentation comments. As far as the compiler is concerned they have no effect on the output other than being aggregated into an XML document. Contract keywords would have no effect on the output other than exposing contract metadata in the Roslyn API for tools such as CC to use.

- Dave
Aug 12, 2014 at 8:18 AM
I see. We attempted to use code contracts earlier in Roslyn, but they couldn't handle the complexity of the scanner, much less the parser, so after some discussions with the team we abandoned them.

Unfortunately, I see a couple issues with your proposal as it stands. First, the code contracts team is not requesting the feature. I'm very reticent about implementing a tooling feature without a stated request from the author of the tool. If they don't use it it would be a lot of work for nothing.

Second, usually tooling-oriented features have more than one obvious consumer. For example, documentation comments are used by the IDE, doxygen, and MSDN, just to name a few. The only other consumers of this metadata that you want are theoretical.

Third, documentation comments can be viewed as a full feature in and of themselves -- just because it's not nice doesn't mean you can't read the generated XML directly. In this case, it's hard to separate your proposed syntactic addition from the Code Contracts utility. What would the metadata look like? Is it solely dictated by the Code Contracts team? That's a red flag already -- designing a feature too closely to one use case smells of overspecialization. Is this metadata consumable by other API surfaces, like reflection? How would we encode this, since .NET doesn't have a direct correlation to contracts?

So overall, this sounds like a lot things against the proposal. Add in the fact that Code Contracts aren't that widely used and it begins to look more suspicious. I would much rather address this as a proposal to add contracts to the language, but having written my Masters thesis on contracts, I also know that could be a massive undertaking -- one which is highly unlikely to take precedent over other suggestions we have pending.
Aug 12, 2014 at 12:31 PM
Isn't it funny that the Entity Framework vNext team is using JetBrains' contracts and not the Microsoft's ones?

https://github.com/aspnet/EntityFramework/blob/dev/src/EntityFramework/Utilities/Check.cs

http://blog.jetbrains.com/dotnet/2012/08/15/contract-annotations-in-resharper-7
Aug 12, 2014 at 12:40 PM
@dsaf: Ugh. There goes any hope at all ;)
Aug 12, 2014 at 1:10 PM
@angocke: Thanks for your thoughtful reply. I understand your point of view and I really can't argue with it. But for the sake of completion, here's some counterpoints anyway :)
I see. We attempted to use code contracts earlier in Roslyn. [snip]
Well that's actually pretty cool. But I hope that just because it didn't work well on the C# compiler doesn't mean that you assume it doesn't work well enough for most apps. In fact, I've used it several times on released apps - a few without really paying any attention to the static analysis results and simply relying on runtime benefits - and it's been a great success for me.
First, the code contracts team is not requesting the feature [snip]
Understood. It would be kind of pointless then, unless it actually goes open source (see Francesco's reply on June 06, 2014).

I dropped a link to this discussion on the CC forum to see if anyone bites :)
Second, usually tooling-oriented features have more than one obvious consumer [snip]
Third, documentation comments can be viewed as a full feature in and of themselves [snip]
Well as it turns out, CC also has a feature that updates XML doc comments with contracts! So all of those tools that are consumers of XML doc comments (including Sandcastle, which already has support for CC doc comments) would also benefit from having contracts in the XML comment files. And theoretically the C# compiler could output the contracts directly into the XML documentation itself, without requiring the CC tools to be installed.

So does that mean that all of the use cases for XML documentation output also apply to Code Contracts? I think so (because I'm biased and it supports my case.)
What would the metadata look like? Is it solely dictated by the Code Contracts team? [snip]
How would we encode this, since .NET doesn't have a direct correlation to contracts?
Well, hasn't DbC been around for a while? I suspect it would just be a few new kinds of nodes that contains typical C# expression nodes. C# basically just needs some form of expression for preconditions and post-conditions (and ideally, invariants as well), with a couple of additional things like being able to refer to return values, previous values and out parameters in expressions. Perhaps the most difficult part would be purity checking of expressions to ensure that they have no side-effects? Though CC doesn't even do that now (it just looks for PureAttribute) and it gets along just fine.

Of course, I'm not an expert. I must assume that you could answer this question way better than me.
Is this metadata consumable by other API surfaces, like reflection?
No: Reflection. The assembly need not contain any contract metadata. (Yea CaaS!)
Yes: IDE, Resharper, custom analysis tools, documentation tools (which theoretically could simply read the metadata from the XML doc comments as mentioned previously)
Add in the fact that Code Contracts aren't that widely used and it begins to look more suspicious. [snip]
How many people wrote iterators in C# before iterator blocks were introduced? Now that it exists in C#, how many devs don't write iterator blocks?
I would much rather address this as a proposal to add contracts to the language, but having written my Masters thesis on contracts, I also know that could be a massive undertaking [snip]
Well even if you were going to do that, then wouldn't the CC team's work provide a great head start?

Thanks,
Dave
Aug 13, 2014 at 12:40 PM
I would really like to see this discussion go forward, but not strictly on code contracts.

The case of static and runtime contracts in .NET are very different.

Static Analysis:

Moves toward easier static analysis are exceedingly good for the language. For the present, writing an app that can handle static analysis is very hard in C#. Roslyn may allow better evaluation of purity and it will be quite interesting to see whether the code contracts team is exploring using Roslyn for analysis, It's interesting, I care, and we're so far away it seems a mirage.

Runtime Analysis

It's not contracts. It's assertions. It's a particular syntax for assertions.

We are in desperate need of a top to bottom rethink of assertions and tracing. We have a tool that allows entirely consumer side control of the information our apps spit out integrated with all the stuff .NET does (exceptions, GC, just about everything else) that we can drop our human understanding of our code into. That understanding of our app is integrated in time with everything else going on with the machine, close in time integrated with a view of the other machines we are interacting with, potentially correlated. And we have this within a semantic set of thinking that makes code more understandable. And it's plenty fast to keep on in production. And there is already a mechanism for multiple audiences (dev and ops).

And almost no one knows about it.
And the tooling sucks.

(ETW and semantic EventSource classes with or without SLAB out of proc listeners)

I would really, really like to see us move toward holistic support for communicating with developers across the entire application unified across debug and production.

I would like to see one part of that support be very similar to DaveDev's use of the current code contract semantics. I would like this to result in code that calls very lightweight semantic methods (so there would probably be a lot of them) that allowed consumer tuning of output during both development and production.

One way to implement this is via "annotations" (the word comes from Java's implementation) and code expansion at compile time into EventSource classes and calls to them. It would also allow XML documentation support and creation of application aware tooling that made it easier for devs and dev/ops to have application specific views of their apps to control ETW collection.

The only pieces of this that aren't currently present are:
  • a common way to do "annotations" (right now you have to roll your own and I don't know who else is doing it)
  • a common syntax for contracts (patterns, standards, expectations)
Combining runtime contracts with other tracing is a different way of thinking, but I think a very useful one.

Kathleen
Aug 14, 2014 at 3:08 AM
Edited Aug 14, 2014 at 3:09 AM
(EDIT: this is not directed at Kathleen or davedev)

Come on-- you're saying that it makes way more sense to use awkward, undiscoverable, incredibly verbose and repetitive static methods to describe the simplest of pre/postconditions in every function, create a member that you never intend referenced by any code anywhere to fill with more awkward and arcane static method calls if, God help you, you must express invariants, than to even consider creating some far more concise equivalents for the compiler in order to make Code Contracts not useless? For heaven's sakes, I've looked at the Reference Source site, you've got Code Contracts throughout the entire framework! Why not make adjustments that would be applicable to the whole framework?! How in the world can you justify not having a language feature because a whole team of smart people figured out how to abuse existing language features in such a way that they could rewrite the output of the "real" compiler to express simple logical assertions about object and method inner workings?

It's one thing to say it's too much work, that you'll consider it in another release, or that you think it just isn't suited for C# and we should wait for Joe Duffy's muzzle to be removed so we can hear about some truly unique and specialized C#-based language that incorporates these kinds of features. But to say that this should be disregarded because it's already 100% handled by a "library" (a library that only works if the output of the compiler is reworked to actually have the features it promises) is simply ignorant.

I've read so much from members of the language design team and have such great respect for the decisions you've made (even with the ones with syntax I don't like, or the dropped ones because of corner cases that caused too much trouble) that I am shocked that you would provide such an absurd response to this glaring hole in the language. If it's a hole in C# that just can't be properly fixed while still looking like C#, I'm OK with you all doing nothing about it. But don't you dare say that the hack called Code Contracts, well-designed as it is, is not a hack but the solution.
Aug 14, 2014 at 1:09 PM
zeldafreak,

I am a bit confused by a few things in your post. I think you have good points beyond the fact that you really, really don't want them to drop code contracts, and you think the current implementation is lacking. Could you clarify a bit, even if you keep the passion.

If you don't know - I don't work for Microsoft, so I can't help you with a "real" answer. However, I'm very, very interested in how people who think about these problems think about them, and why so many people don't think about them.

IT seems to me that the current code contracts do two things - although they use the same code to do both things.
  • run-time code contracts, which is actually a set of semantics for assert style development time tracing
  • design-time code contracts which evaluate source code as an attempt at correctness, but some of the purity assumptions are based on claims
Are you talking about one or the other of these or both? (I find most people perceive code contracts largely as one or the other)

You mention a couple of things (a member you never intend referenced, invariants), in relation to this discussion about code contracts. Aren't these features that would be better fixed completely separately from code contracts? Isn't using code contracts to make a claim, rather than a type that enforces that claim a hack in and of itself?

Kathleen
Aug 14, 2014 at 1:18 PM
Edited Aug 14, 2014 at 1:38 PM
Can I point you to an alternative approach Code Contract (Language Support) that is suitable for both C# and vb.net.

@davedev using the alternative approach you could do the following.
public interface IDoThings
{
  void DoSomething( int x #0, int y #1)
    contract { [0]{ x >= 0 }
               [1]{ x < y  }
             }
  foo! DoSomethingElse( Baz! o )
    contract { [0]{ensures result.Baz == o } }
    /* [ ]{ o isnot null }
       [ ]} ensure result isnot null }
       are implied via the type postfix operator !
    */
}
Aug 14, 2014 at 7:25 PM
Sorry if I was unclear. I was merely taking issue with what I perceived to be the sentiment that any kind of compiler support for Code Contracts (I'm being deliberately vague because I don't want any specific keyword or language feature to distract from my point) is precluded by the language design guideline of (to paraphrase) "if it can be handled by a library, let it be handled by a library rather than changing the language".

When you use Code Contracts, you use code elements from the library to explicitly state certain intentions and information about methods that can be difficult (or impossible) for a compiler or static analysis tool to determine on its own. Those code elements (static functions like Contract.Requires and the "member you never intend to reference" containing class invariants) are NOT library invocations in any sense of the word. They serve as markers. A tool looks for them in your compiled code and turns them into assertions so they are enforced at run-time, and static analysis tools look for them at compile-time/during development to try to indicate to the developer as soon as possible whether or not he is satisfying the contracts (constraints) he explicitly stated. (the runtime and design-time features you mention).

I do not believe that this kind of hack constitutes a "library solution," so a discussion about the merits of language features that provide similar function as the Code Contracts package in whole or in part should not be disregarded by virtue of there being a library created years ago that provided the features using a roundabout and completely impractical means. (Mostly because the the compile-step adds way too much time to an already too long REPL in Visual Studio, but also because it abuses language features like static methods to accomplish something that is more like an attribute, and is far too verbose for it to gain any widespread use.) And I further believe it should be given a higher priority since the entire .NET Framework has already implemented Code Contracts, so the argument that it should not be considered for language enhancement because it is unpopular has no basis either.

All of this was written in response to angocke's comments about "not wanting to add a feature that even the tooling provider hasn't requested." But perhaps that's because I don't see Code Contracts as a library or set of tooling, but a concept I would like to express in my type system and today, it's simply impractical. Perhaps a compromise could be struck that would enhance Roslyn in order to make things like Code Contracts easier to create and not make the REPL loop 3-10x longer just to add the run-time checks.
Aug 15, 2014 at 6:49 PM
Edited Aug 15, 2014 at 7:03 PM
whoops wrong topic
Oct 25, 2014 at 10:32 AM
Edited Oct 25, 2014 at 10:32 AM
dsaf wrote:
Isn't it funny that the Entity Framework vNext team is using JetBrains' contracts and not the Microsoft's ones?

https://github.com/aspnet/EntityFramework/blob/dev/src/EntityFramework/Utilities/Check.cs

http://blog.jetbrains.com/dotnet/2012/08/15/contract-annotations-in-resharper-7
To me this shows that there is a real demand for defining a common, language built in notation of code contracts that any tool can use, else the proliferation of proprietary notations will obfuscated our code with contracts of all flavors, transforming an excellent, very helpful thing into a burden.
Oct 25, 2014 at 7:23 PM
tomenglert wrote:
else the proliferation of proprietary notations will obfuscated our code with contracts of all flavors, transforming an excellent, very helpful thing into a burden.
Indeed, that already hit me especially in the case of ASP.NET vNext since when overriding methods this automagically leads to visual studio generating a method stub with the [NotNull] Attribute on the parameters which can't be accessed since they are internal. This breaks both: the contract and usability.
Oct 27, 2014 at 7:44 AM
Edited Oct 27, 2014 at 8:52 AM
I see. We attempted to use code contracts earlier in Roslyn, but they couldn't handle the complexity of the scanner, much less the parser, so after some discussions with the team we abandoned them.
 
We don't need integration Code Contracts and Roslyn: it's a bad idea to combine compiler and analyzer tools. We need to human-readable contract in code with the simple way to extract metadata for analyzing.

Like in Eiffel or Nemerle:
public IEnumerable<T> Work(IEnumerable<Employee> employees)
    where T: Product
    requires employees != null
    ensures result != null & result.All(product => product != null)
{
    foreach (var employee in employees)
    {
        yield return employee.DoSomethingPlease<T>();
    }
}
but not like now:
public IEnumerable<T> Work(IEnumerable<Employee> employees)
    where T: Product
{
    if (employees == null)
    {
        throw new ArgumentNullException("employees");
    }
    Contract.Ensures(Contract.Result<IEnumerable<T>>() != null & Contract.ForAll(Contract.Result<IEnumerable<T>>, (T product) => product != null);
    Contract.EndContractBlock();
    foreach (var employee in employees)
    {
        yield return employee.DoSomethingPlease<T>();
    }
}
even it just rewrite code to last version
 
I would much rather address this as a proposal to add contracts to the language
 
I have not tried to use Roslyn, but it sounds like we have the way to add our “vendor specific” extensions to the language, C# for example. And if I right, it mean what all previous respondents going in the wrong direction: you don't need to integrate Code Contracts to Roslyn, but Code Contracts team need to use Roslyn in next version of their extension.
Oct 27, 2014 at 8:23 PM
Fully agree.
The discussion started with "Are there any plans to add Code Contract keywords to C#" - and it's in the topic "C# Language Design".
I'm reading this discussion more like a demand to add a readable contract specific notation to .Net languages rather than to build an analyzer into Roslyn.
Oct 27, 2014 at 8:54 PM
Edited Oct 27, 2014 at 9:09 PM
Yep, something like LINQ
Nov 13, 2014 at 1:27 PM
How about Spec#/Sing# resurrection?
Nov 13, 2014 at 2:00 PM
I think it's the domain of metaprogramming. Suppose you have invented a C#-derived metaprogramming language for Code Contracts:
public IEnumerable<T> Work(IEnumerable<Employee> employees)
    where T: Product
    requires employees != null
    ensures result != null & result.All(product => product != null)
{
    foreach (var employee in employees)
    {
        yield return employee.DoSomethingPlease<T>();
    }
}
Your meta-compiler will translate the preceding meta-code into the following C# implementation code:
public IEnumerable<T> Work(IEnumerable<Employee> employees)
    where T: Product
{
    if (employees == null)
    {
        throw new ArgumentNullException("employees");
    }
    Contract.Ensures(Contract.Result<IEnumerable<T>>() != null & Contract.ForAll(Contract.Result<IEnumerable<T>>, (T product) => product != null);
    Contract.EndContractBlock();
    foreach (var employee in employees)
    {
        yield return employee.DoSomethingPlease<T>();
    }
}
If you just want to implement a prototype, try https://roslyn.codeplex.com/discussions/570635 :)