Expert to Expert: Contract Oriented Programming and Spec#

The Discussion

• 

  AWESOME! Thanks for this video, Charles. I love it already before having watched it *downloading*

• 

  LOW RES FILE
  
  MP4
  
  ZUNE

• 

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

• 

  Glad you're liking this one. I know I really enjoyed the conversation (and learned a lot). It's too early to tell what will become of this type of functionality and how it will map to our general purpose programming languages like C# and VB.NET...
  
  Keep in mind that Spec# is a research implementation and not intended for product-quality uses. The concept of Contract Orientation is alive and well today in langauges like Eiffel (though the implementation is different than Spec#'s...).
  
  
  Stay tuned...
  C

• 

  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.

• 

  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?

• 

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

• 

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

• 

  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:
  
  

• 

  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?

• 

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

• 

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

• 

  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.