Expert to Expert: Contract Oriented Programming and Spec#

very cool, thanks for the video

That was great, one of the most interesting videos for me in awhile..

I'd love to start working on this, I have some questions, is this based on C# 3.0? or is this an invariation of C# 2.0?

Its fascinating to think that maybe .NET, or I guess maybe even a predecessor to .NET could actually bake this sort of advanced contract into its native language..

Other than that, I'm really interested in seeing how far this can go to being an "alternative" to C# in some scenarios, or perhaps how languages like C# and VB can start to introduce these as core specifications..

This really is exciting stuff (in fact, I created a Channel9 user account just to respond to this video). Charles, I realize this isn't production-ready, but I can't tell you how much I'd like to start using this in my own work now.

I had the same question as stevo_ - What version of C# is this based on? Perhaps someone on the Spec# team can enlighten us on which, if any, newer features of C# are not currently supported in Spec#.

After the steady stream of language and CLR enhancements we've enjoyed--nullable types, generics, and all of the great new enhancements that have come with the dawn of LINQ--this seems like a natural next step. I'm very hopeful Microsoft will bake Design by Contract support into a future version of the CLR.

Here's my vote to see this make it's way into C# 4 and .NET 4.

I watched it yesterday evening. And now, back at work I already wished I had the Spec# features
Great interview, keep the 'Going Deep' stuff comming!

En de oranje das voor Koninginnedag, super Eric!
(translation: and the orange tye for Queens Day, super Eric!)

Hi littleguru,

There are two Design by Contact frameworks I know of that you can use today in C#. They both enforce checks at runtime, but take very different approaches and will appeal to very different audiences.

Kevin McFarlane has created an easy-to-use API that always enforces checks at runtime via calls to a Check object, such as:

Check.Require(0 < x < 5);

Check.Ensure(result < 3);

Check.Invariant(B.a > 0 and B.b > 0);


Philip Laureano offers a more complicated Design by Contract library as part of a larger library called LinFu. He uses a language-neutral, attributes-based approach for declaring contract checks. The advantage--or disadvantage, depending on your point of view--to Philip's approach is that the library is completely ignorant of the contract checks you assign, which means that when you call your library as normal, none of the checks will be made. In order for the checks to actually be enforced, you must use LinFu to create proxy versions of your classes with all the checks injected into the proxies. I get the impression this DbC approach is best used in conjunction with some sort of Dependency Injection framework, either LinFu's own or something like Spring.NET or Castle Windsor.

If you want a simple and lightweight API that bakes checks into your library so that they are always performed regardless of the caller, Kevin's API is probably your best bet. If you require your checks to be completely separate from your library to the point that they are optional, and if you're already working on an enterprise project using Dependency Injection, take a look at LinFu.DesignByContract2.

Hope that helps,
Adam.

Intersting Stuff. The media length looked too much but it was a short discussion at the end with many things left unaddressed.

Handling Overloaded Function

For overloaded function(s), there must be a single case specification, or each function must be addressed seperately.

Moreover, Unlike Java, C# allows funtion overloading based upon return types, which When called in code, tend to confuse reader/compiler.

For example,to multiply 2 integers, a class can include following overloaded functions:

..
int mult(int, int);  // call if result is less than max (int), return int
long mult(int, int);  // call if  max (int) <=result<=max (long), return long
float mult(int, int);  // call if  max (long) <=result<=max (float), return float
double mult(int, int);  // call if  max (long) <=result<=max (double), return double
...

Compiler Intelligence conflicting software design principles

This is a Programmer responsibility and Compiler responsibility case, that is, what a programmer need to specify and what a compiler must assume.

This C/C++ code is self explanatory without any documentation/comments

...
unsigned x=[some expresion];
..
if (x) 
...
...

The C/C++ compilers are intelligent enough to assume that condition will execute if x is a positive integer, and Java/ C# compilers require an explicit condition for that adding burden to programmer.

A fun case

As discussedm, Spec is applied on C code to catch/handle every possible case. Learning the languaage, this is the first piece of code developers eneter:

#include <stdio.h>

int main()
{
 printf("xyz"); //xyz can be any string
 return 0;
}

Going deep in the language, at a stage programmer discover that printf() in fact returns a value, which is usually a positive integer but in the most rare case, it can be negative indicating an exception. Applying spec on rare cases like this, perhaps once in a lifetime sort of case...

That was about compiler efficiency and intelligence, i.e.,  a compiler intelligent enough to assume certain conditions. You can say limiting a programmer creativity by restricting to a certain struct like bool or allowing him the choice of using bool if required.

The code provided requires two explicit test conditions to be entered in Java/C# compilers and your question will still remain unanswered.

if (S_OK)
 ....;
else if (S_FAIL)
 ......;


In Java/C#

....;  //get some value for x somehow
if (x==S_OK)
 ....;
else if (x==S_FAIL)
 ....;

In both versions, you cannot answer unless you have some hint on constants, but at least one extra statement and two explicit test conditions due to developer in Java/C# version.

How did you integrate with the Visual Studio environment? Would it be possible to get a simple sample/tutorial on VS SDK?

First of all, thanks for a very interesting video! I have a question about the way invariants are implemented in Spec#. Traditionally (i.e., in Eiffel), invariants are only checked when you exit a method that was called from a different object, so you can break an invariant somewhere in the middle of a method or even have a private method that breaks an invariant every time. Was there any specific design issue that made you change the way invariants work and enforce them after every statement, which led to the introduction of the expose block?

Wow, great video, charles & erik. It was really exiting to see Spec#. I wonder if it will be integrated (fully/partly) into C#.

To Windows 3.0 in Vista. Well, theres a Windows 3.0-Like File-Dialog still in Vista in the font-management.

Goto "Control-Panel" -> "Apperance and Personalisation" -> "Fonts", right-click on the panel, choose "Install New Font".

Screens:

Wierd to see Eric in a suit Nice tie though.

The first question people have regarding contracts is, why bother? The speakers addressed this by explaining how much money Microsoft saved in manual testing time. But there are other savings as well.

By specifying assumptions explicitly, the design improves. You move from fuzzy verbal communication to concise, precise communication about the behavior and expectations of code. This has the same benefits as writing documentation before code, or writing tests before code. It clarifies the design.

Even without compile-time or run-time contract checks, a contract allows one to view classes or methods as black boxes with precise behavior, ignoring internal details. This helps to logically determine if a design functions correctly.

Another benefit is reduced debugging time. If you use only run-time contract checks, you eliminate the time normally spent trying to narrow down a bug -- you find it earlier, before it is manifested in peculiar ways. If you have compile time checking as well, as in spec#, the same bug would never occur -- it would spotted by the compiler.

The work done by the spec# group is important. I hope it goes into products as soon as possible.

littleguru wrote:

Still, you didn't answer the question on S_OK and S_FAIL and therefore I will tell you what they are: S_OK == 0 and S_FAIL == 1 - interesting, isn't it?

this is platform specific code, or constants defined on a specific platform, the same constants may have different value in C/C++ compiler running on Linux/Solaris or some other platform or they might not exist at all. We were never interested in win32 or platform specific discussion, here.

Experts to experts? Indeed! I didn't get a point of Spec#... Absolutely. Perhaps because I'm not an "expert"...

PS: Those guys look like absolute geeks... Crazy eyes, crazy hairdressings...

The implications of this type of programming language are unignorable. It is doubtless that it's programming syntax will spead into C# and WCF especially. You really need to have programmed C++ to fully appreciate just what level of control you are given at compile time. I have been toying around with possibly trying dynamically typed languages like RoR but I shall NEVER, as long as this continues to be developed.

This isn't so much "patterns and practices" for applications, but for programming. Once some formal ground rules are established, one can indeed write better, faster, more secure, less buggy, eloquent and performant code.

Well Done to John, Paul, Ringo...

"Is this based on C# 3.0? or is this an invariation of C# 2.0?"
From what I remember from other interviews it is based on C# 2.0.

Another interesting interview (which I think is where I got the above from) can be found at http://www.hanselminutes.com/default.aspx?showID=128

Very, very, very, very cool stuff!

I would love to write software this way!

You look nice in a suit Erik!

aJanuary wrote:

"Is this based on C# 3.0? or is this an invariation of C# 2.0?"
From what I remember from other interviews it is based on C# 2.0.

Another interesting interview (which I think is where I got the above from) can be found at http://www.hanselminutes.com/default.aspx?showID=128

I really don't see what the obsession with whether it's a .NET 2.0 or 3.0 invariant.

A quick read of the Spec # website tells you that that it is an extension (Variation) of the C# language, so using the word invariant is incorrect. Use the word invariant with Objects when programming Spec#.

Furthermore, the Research Team utilise MSIL, so there is no reason that is unimplemantable in Visual Basic or other .NET aware language. If you or steveo_ are that curious install the Spec# VS2005 or 2008 versions from the website, and have a quick check to see whether you can write/use extension methods, automatic properties, partial methods anonymous types or object initialisers. That should satisfy your curiosity, although the 'meat and potatoes' is definitely with object invariants (.NET 2.0 and 3.0 both have objects - and nulls) so I would certainly deem this a curiosity, but wholly inconsequential to understanding Spec#.

vesuvius wrote:



aJanuary wrote: "Is this based on C# 3.0? or is this an invariation of C# 2.0?" From what I remember from other interviews it is based on C# 2.0. Another interesting interview (which I think is where I got the above from) can be found at http://www.hanselminutes.com/default.aspx?showID=128

I really don't see what the obsession with whether it's a .NET 2.0 or 3.0 invariant.

A quick read of the Spec # website tells you that that it is an extension (Variation) of the C# language, so using the word invariant is incorrect. Use the word invariant with Objects when programming Spec#.

Furthermore, the Research Team utilise MSIL, so there is no reason that is unimplemantable in Visual Basic or other .NET aware language. If you or steveo_ are that curious install the Spec# VS2005 or 2008 versions from the website, and have a quick check to see whether you can write/use extension methods, automatic properties, partial methods anonymous types or object initialisers. That should satisfy your curiosity, although the 'meat and potatoes' is definitely with object invariants (.NET 2.0 and 3.0 both have objects - and nulls) so I would certainly deem this a curiosity, but wholly inconsequential to understanding Spec#.

Pretty ironic post to say you summed up "why ask a question when you can google it" with an overzealous post.. its almost on the level of quoting someone with "stop spamming"...

Believe it or not, people actually want to discuss and show interest.. not just watch then google the rest.. I wanted to post mainly to show that I appreciated their time to do the video, and to work on spec# in the first place..

And for the record, its pretty obvious why someone may ask, is this based on c# 2 or 3, since no point did it state this was an extension to c# in general, vs a sort of 'branch'..

stevo_ wrote:



vesuvius wrote:  aJanuary wrote: "Is this based on C# 3.0? or is this an invariation of C# 2.0?" From what I remember from other interviews it is based on C# 2.0. Another interesting interview (which I think is where I got the above from) can be found at http://www.hanselminutes.com/default.aspx?showID=128 I really don't see what the obsession with whether it's a .NET 2.0 or 3.0 invariant. A quick read of the Spec # website tells you that that it is an extension (Variation) of the C# language, so using the word invariant is incorrect. Use the word invariant with Objects when programming Spec#. Furthermore, the Research Team utilise MSIL, so there is no reason that is unimplemantable in Visual Basic or other .NET aware language. If you or steveo_ are that curious install the Spec# VS2005 or 2008 versions from the website, and have a quick check to see whether you can write/use extension methods, automatic properties, partial methods anonymous types or object initialisers. That should satisfy your curiosity, although the 'meat and potatoes' is definitely with object invariants (.NET 2.0 and 3.0 both have objects - and nulls) so I would certainly deem this a curiosity, but wholly inconsequential to understanding Spec#.

Pretty ironic post to say you summed up "why ask a question when you can google it" with an overzealous post.. its almost on the level of quoting someone with "stop spamming"...

Believe it or not, people actually want to discuss and show interest.. not just watch then google the rest.. I wanted to post mainly to show that I appreciated their time to do the video, and to work on spec# in the first place..

And for the record, its pretty obvious why someone may ask, is this based on c# 2 or 3, since no point did it state this was an extension to c# in general, vs a sort of 'branch'..

I did not Google it,  I simply read what Charles posted. If you read that initial post, you will find that that's where I extrapolated my info. There is a very clear link to the Spec# site with additional info posted by Charles.

Other information was deduced from watching the video, and my post remains correct. Your clearly misunderstood the meaning and usage of the word invariant, and are "barking up the wrong tree" with regard to .NET 2.0 and .NET 3.0 as their are inconsequential.

How can you show appreciation for watching the video by going ahead and showing you misunderstood it? These are pretty smart guys, and I find it offensive you'd see it as important to ask such misconstructed information.

Read Charles's initial post properly. Don't try save face posting ambiguous and poorly explained posts. I have made myself abundantly clear.

vesuvius wrote:



I did not Google it,  I simply read what Charles posted. If you read that initial post, you will find that that's where I extrapolated my info. There is a very clear link to the Spec# site with additional info posted by Charles.

Other information was deduced from watching the video, and my post remains correct. Your clearly misunderstood the meaning and usage of the word invariant, and are "barking up the wrong tree" with regard to .NET 2.0 and .NET 3.0 as their are inconsequential.

How can you show appreciation for watching the video by going ahead and showing you misunderstood it? These are pretty smart guys, and I find it offensive you'd see it as important to ask such misconstructed information.

Read Charles's initial post properly. Don't try save face posting ambiguous and poorly explained posts. I have made myself abundantly clear.

I never said anything about .NET 2.0 or .NET 3.0... I was talking about C# 2.0 and C# 3.0.. I asked nothing about spec# and a version of .NET... I know spec# works against CIL specification, I however did want to know if spec# had all the language features of C# 3.0, or if it was features of C# 2.0...

You do understand the difference there son?

And your post just reiterates again "Well I 'got' it, then you should of as well.", sorry- we're obviously not all as hyper-intelligence as you are..

You don't come here and dictate what people can ask, so politely- you can get f--ked.. you weirdo.

Good show guys.  The spec# team reminded me of the NASA guys in the 60s.  Very retro.  Nice tie Eric.  Look forward to this in c# 4.0.

aJanuary wrote:

"Is this based on C# 3.0? or is this an invariation of C# 2.0?"
From what I remember from other interviews it is based on C# 2.0.

Another interesting interview (which I think is where I got the above from) can be found at http://www.hanselminutes.com/default.aspx?showID=128

In fact it says in that very interview (about 3 mins in) it's a superset of C# 2.0 and rather than a superset of C# 3.0. They also mention shortly after (and talk about it a little in the video )they are looking at a non-language specific solution.