Introduction to Code Contracts [Melitta Andersen]

Introduction to Code Contracts [Melitta Andersen] | Tmao Coders

Introduction to Code Contracts [Melitta Andersen] | Tmao Coders — Wed, 12 Nov 2008 03:02:53 GMT

PingBack from http://www.tmao.info/introduction-to-code-contracts-melitta-andersen/

re: Introduction to Code Contracts [Melitta Andersen]

snprbob86 — Wed, 12 Nov 2008 07:57:23 GMT

C# and Python are tied for my favorite languages. Attributes are cool, but Python's decorators are cooler.

Check out these simple precondition and postcondition decorators:

http://wiki.python.org/moin/PythonDecoratorLibrary#head-e1a9273f88f2fc4e39faf297279f4d1dc8b2ae66

.NET 4.0's game-changing feature? Maybe contracts...

Jon Skeet: Coding Blog — Wed, 12 Nov 2008 12:28:40 GMT

Update: As Chris Nahr pointed out, there's a blog post by Melitta Andersen of the BCL team explaining

re: Introduction to Code Contracts [Melitta Andersen]

Jonathan Pryor — Wed, 12 Nov 2008 22:52:33 GMT

If I make one API suggestion (which may already be followed, I have no idea)...

Ensure

You mention:

"They also have an overload that takes a string parameter as a message for when the contract is false."

Please, *please*, PLEASE make the overloaded method take a "string format, params object[] args" argument list and not just a string. For simple code there will be no difference for the developer, but if you ever need to "format" the message string it looks far cleaner than needing to insert string.Format(). Compare:

CodeContract.Requires(parameter >= 0, "parameter value {0} must be greater than 0", parameter);

To:

CodeContract.Requires(parameter >= 0, string.Format("parameter value {0} must be greater than 0", parameter));

.NET 4.0 Contracts

Andrew Stopford's Weblog — Thu, 13 Nov 2008 01:40:42 GMT

First showed at the PDC as a part of this Pex session was support for contracts , if you have seen the

re: Introduction to Code Contracts [Melitta Andersen]

Steven the .NET Junkie — Thu, 13 Nov 2008 23:19:26 GMT

This is the greatest news I heard in years. I was very exited about the things Spec# could bring us, but bringing verification to the rest of the framework is superb. The most development teams I help use C# and moving to another language wouldn’t be feasible for them.

I have a question though. I’m a big believer of the Framework Design Guidelines and they state that a failing precondition should throw an ArgumentException (or descendant). How does Contracts deal with this?

I don’t think it’s necessarily to add a ‘string, parms object[]’ overload to the Requires and Ensures methods, as Melitta Andersen suggests. Using a string.Format() would be sufficient when the post-compilation process changes the implementation to something like ‘if (conditions) throw new Exception(string.Format(…))’. How is this currently implemented?

re: Introduction to Code Contracts [Melitta Andersen]

Judah Himango — Fri, 14 Nov 2008 22:45:32 GMT

First, great news! I think this is *the* best news coming out for .NET 4. It's something I've wanted for years.

Question:

Care to talk a little bit about how this works for interfaces, where you can't actually put code inside your methods?

interface IFoo

{

DoSomething(string s)

{

CodeContract.Requires(s != null);

};

}

In the above interface, the compiler will issue an error; you can't have code statements inside an interface.

(This is another argument in favor of using attributes, as they are allowed in interfaces.)

Another question:

If attributes were powerful and expressive enough, would the team consider implementing code contracts using attributes? I ask because there has been a lot of feedback on the MS Connect website to allow more expressiveness inside attributes. See

https://connect.microsoft.com/VisualStudio/feedback/ViewFeedback.aspx?FeedbackID=254057

re: Introduction to Code Contracts [Melitta Andersen]

BCLTeam — Sat, 15 Nov 2008 02:22:51 GMT

Hi snprbob86,

Thanks for passing along the link to the Python decorators. That looks like an interesting contract system, and seems to have some of the same concepts as the one we implemented. For example, the ability to have contracts at debug time only or the ability to incorporate functions into conditions to make them more expressive are elements of our own code-based implementation.

Thanks,

Melitta

re: Introduction to Code Contracts [Melitta Andersen]

BCLTeam — Sat, 15 Nov 2008 02:24:27 GMT

Hi Jonathan,

Thanks for the API suggestion. It's an interesting idea, and does make the code a little neater. However, at this point we're trying to keep the code contract APIs as minimal as possible. This makes it less complicated for the tools to extract the conditions. Overloads with more parameters make the task more difficult. It's something we'll think about, but we may not be able to make it happen in this release.

Thanks,

Melitta

re: Introduction to Code Contracts [Melitta Andersen]

BCLTeam — Sat, 15 Nov 2008 02:26:11 GMT

Hi Steven,

You have some good questions here. We don't have any official Framework Design Guidelines yet for when to use code contracts and when to use ArgumentExceptions. While many of us are fans of contracts, clearly we can't just say "change all of your existing preconditions to code contracts," because there is often already infrastructure in place around throwing these ArgumentExceptions and there is too much potential to break people. This is a brand new feature, and we're doing some experimentation internally to find out what works best so that we can make more informed recommendations.

As for your question about how we implement the behavior of code contracts under the hood, we don't convert it to an exception. In the CTP bits we check the condition and then tear down the process if they fail. We use the string as part of a message to the user when this happens. As I mentioned above, we're considering options to make this behavior more flexible, and especially to make it friendlier to hosts.

Thanks,

Melitta

re: Introduction to Code Contracts [Melitta Andersen]

BCLTeam — Sat, 15 Nov 2008 02:27:34 GMT

Hi Judah,

Thanks for pointing out that I neglected to mention how code contracts work on interfaces. As you've said, you can't put code into interface methods. What you do is create a separate class to contain the contracts that <i>explicitly</i> implements the interface. Then you link them with a pair of attributes: [ContractClass(Type)] and [ContractClassFor(Type)]. For example you could have an interface IFoo with a class IFooContract that contains the contracts.

[ContractClass(typeof(IFooContract))]

interface IFoo

{

int DoSomething(string parameter);

}

[ContractClassFor(typeof(IFoo))]

sealed class IFooContract : IFoo

{

int IFoo.DoSomething(string parameter)

{

CodeContract.Requires(parameter != null);

CodeContract.Ensures(0 <= CodeContract.Result<int>());

throw new NotImplementedException("This method is only for interface contracts. Do not call");

}

As for your question about attributes, if they were powerful enough, we certainly would have considered using them to implement contracts, though I can't say for sure what we would have decided. As it is, we don't know of any plans for more expressive attributes, and even if they do come along later, we would already have an established contracts system. There would by that point be many factors to take into consideration when looking at adding attribute support.

Thanks,

Melitta

re: Introduction to Code Contracts [Melitta Andersen]

Steven the .NET Junkie — Sat, 15 Nov 2008 16:57:04 GMT

I don't like using attributes for the contracts. It’s almost impossible to do compile time checking on them, and they’re very verbose. I've seen Spec# and it has the ideal language syntax. I hope this syntax makes it to C# 5.0. (Well… I'm really hoping C# 4.0 will have all this, but I know this isn't going to happen ;-)).

re: Introduction to Code Contracts [Melitta Andersen]

int19h — Sun, 16 Nov 2008 12:24:30 GMT

Judging by its past track, one .NET language that will almost certainly provide syntactic sugar for the library contracts is Delphi Prism (aka RemObjects Oxygene). They do in fact already have "require", "ensure", and "invariant" keywords, so it would make sense for them to plug them into those BCL bits for .NET 4.0, and extend the syntax to cover all other cases ("require ... on raise ..." etc).

Various Links

Mike Taulty's Blog — Thu, 20 Nov 2008 23:02:35 GMT

I've been catching up on my blog reading...interesting stuff I came across; PNRP in Windows 7 being...

契約によるプログラミング.NET

biac のそれさえもおそらくは幸せな日々@nifty — Tue, 25 Nov 2008 18:08:46 GMT

InfoQ に日本語記事が載ったので f(^^; .NET 4 の新機能を探る：コード契約作者 Jonathan Allen, 翻訳者金森諭投稿日 2008年11月22日午前12時53分契約による設計は静的型付けのように、コンパイル時に検証されないと一定の動作を実行することができないという考え方だ。契約

re: Introduction to Code Contracts [Melitta Andersen]

Flavien Charlon — Mon, 01 Dec 2008 19:11:10 GMT

Hi,

Contracts are really nice.

In order to be able to use them properly though, we will need pre and postconditions from all the classes we use in our program, for exemple, List<T>.Count is always positive or zero.

Are you going to update the whole BCL with code contracts for .NET 4.0? This sounds like a huge work, but without that, contracts won't be usable at their full potential.

My second question is why C# wouldn't have a syntax that would get translated into CodeContracts upon compilation.

With this we get a good langage support in C#, as well as the ability to have it supported accross all CLR langages.

Preview of Code Contract Tools Now Available [Melitta Andersen]

BCL Team Blog — Tue, 24 Feb 2009 02:02:52 GMT

In my Introduction to Code Contracts post, I mentioned that the tools to enable runtime checking and

Preview of Code Contract Tools Now Available

CLR Team Blog — Wed, 04 Mar 2009 23:06:25 GMT

We’ve mentioned Code Contracts over on the BCL Blog a few times now, but never yet on the CLR Blog. Basically,

Relacja z C2C (Communities to Communities) 2009

. jak .NET by Maciej Aniserowicz — Mon, 16 Mar 2009 01:59:14 GMT

Dzień: 14 marca 2009. Miejsce: Wydział Biologii UW. Wydarzenie: druga edycja konferencji Communities

Relacja z C2C (Communities to Communities) 2009

. jak .NET by Maciej Aniserowicz — Mon, 16 Mar 2009 02:00:35 GMT

Relacja z C2C (Communities to Communities) 2009