Comment Feed for Expert to Expert: Contract Oriented Programming and Spec# (Going Deep on Channel 9)

Re: Expert to Expert: Contract Oriented Programming and Spec#

aJanuary — Sat, 31 May 2008 17:54:25 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

staceyw — Fri, 30 May 2008 11:51:35 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

stevo_ — Fri, 30 May 2008 08:29:29 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

vesuvius — Fri, 30 May 2008 06:48:45 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

stevo_ — Thu, 29 May 2008 20:45:53 GMT

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'..

Re: Expert to Expert: Contract Oriented Programming and Spec#

vesuvius — Thu, 29 May 2008 11:07:16 GMT

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#.

Re: Expert to Expert: Contract Oriented Programming and Spec#

Maddus Mattus — Thu, 29 May 2008 10:55:43 GMT

Very, very, very, very cool stuff!

I would love to write software this way!

You look nice in a suit Erik! [H]

Re: Expert to Expert: Contract Oriented Programming and Spec#

aJanuary — Thu, 29 May 2008 10:25:21 GMT

"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

Re: Expert to Expert: Contract Oriented Programming and Spec#

vesuvius — Thu, 29 May 2008 10:23:04 GMT

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...

Re: Expert to Expert: Contract Oriented Programming and Spec#

littleguru — Thu, 29 May 2008 07:06:36 GMT

umer_a wrote:

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.

Hehe. But you know that's why I'm for one bool. True, False that is. :)

But we are discussing things here that are only slightly related to the topic...

Re: Expert to Expert: Contract Oriented Programming and Spec#

BlackTiger — Thu, 29 May 2008 07:02:35 GMT

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... [H]

Re: Expert to Expert: Contract Oriented Programming and Spec#

umer_a — Thu, 29 May 2008 00:16:06 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

Frank Hileman — Wed, 28 May 2008 22:56:21 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

aJanuary — Wed, 28 May 2008 21:36:27 GMT

Wierd to see Eric in a suit :S Nice tie though.

Re: Expert to Expert: Contract Oriented Programming and Spec#

littleguru — Wed, 28 May 2008 21:18:58 GMT

umer_a wrote:

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.

if (x)

works in C#/JAVA if x is bool... if you have an int you need to check it against another value to "convert" it to a bool but that's more natural.

For me using an int as a bool is a little bit confusing. If you take CS theory a bool is a bit and not an int. It could only be 1 or 0, whereas

if (y + i + k)

could be anything within the min and max value of the int, which is weird!

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?

Re: Expert to Expert: Contract Oriented Programming and Spec#

GamlerHart — Wed, 28 May 2008 21:00:34 GMT

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:

Re: Expert to Expert: Contract Oriented Programming and Spec#

ilmar — Wed, 28 May 2008 20:14:05 GMT

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!)

Re: Expert to Expert: Contract Oriented Programming and Spec#

onodera — Wed, 28 May 2008 19:46:36 GMT

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?

Re: Expert to Expert: Contract Oriented Programming and Spec#

Moshe — Wed, 28 May 2008 16:50:23 GMT

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

Re: Expert to Expert: Contract Oriented Programming and Spec#

umer_a — Wed, 28 May 2008 15:31:14 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

littleguru — Wed, 28 May 2008 15:09:27 GMT

adamjcooper wrote:

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.

...

Adam.

Thanks for sharing. The two frameworks seem very primitive compared to Spec#, but not everyone has the time to write a new compiler with IDE integration. The first one is even more like an assert(...) thing.

umer_a wrote:
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.

I don't know if that can be said as "smart"... This is more like a historical thing and somebody new to C/C++ doesn't know that > 0 means true and 0 represents false (and that a negative value might be an error code)... That's knowledge that you gain over time.

It's also very confusing for people who are new to C/C++ to see checks like this (at least it was for me):

int i = j + y + z;

if (i)
{
// do something.
}

Also, I find it interesting that this "smartness" will not always work. Especially if you have something like this:

if (S_OK)
// ...
else if (S_FAIL)
// ...

Which one do you think is entered? (just by looking at the variable names).

Having a Boolean type like in .NET is way better, IMHO. And having just ONE Boolean type is very important, not like in the SDKs based on C/C++ where you have tons of different representations for something that worked out and something that didn't...

Re: Expert to Expert: Contract Oriented Programming and Spec#

umer_a — Wed, 28 May 2008 12:21:43 GMT

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...

Re: Expert to Expert: Contract Oriented Programming and Spec#

adamjcooper — Wed, 28 May 2008 12:17:14 GMT

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.

Re: Expert to Expert: Contract Oriented Programming and Spec#

littleguru — Wed, 28 May 2008 09:08:03 GMT

Wow this was a load of cool features and questions!

This video made wonder the following: are there tools around that do the stuff that the team does with their checker already on current C# code; or MSIL code? Anybody having come across a tool similar to their checker?

Re: Expert to Expert: Contract Oriented Programming and Spec#

adamjcooper — Tue, 27 May 2008 22:30:59 GMT

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.