Entries:
Comments:
Posts:

Loading User Information from Channel 9

Something went wrong getting user information from Channel 9

Latest Achievement:

Loading User Information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

Expert to Expert: Contract Oriented Programming and Spec#

Download

Right click “Save as…”

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software.  Spec# is pronounced "Spec sharp" and can be written (and searched for) as the "specsharp" or "Spec# programming system".  The Spec# system consists of:


The Spec# programming language.  Spec# is an extension of the object-oriented language C#.  It extends the type system to include non-null types and checked exceptions.  It provides method contracts in the form of pre- and postconditions as well as object invariants.

The Spec# compiler.  Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.

The Spec# static program verifier.  This component (codenamed Boogie) generates logical verification conditions from a Spec# program.  Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.

A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.

The Spec# programming system is being developed as a research project at Microsoft Research in Redmond, primarily by the Programming Languages and Methods group.

Here, Expert to Expert guest expert and programming language guru Erik Meijer chats with MSR researchers and spec# designers Wolfram Schulte,  Rustan Leino and Peter Mueller. We dig into the details of Spec# and contract oriented programming in general. Plenty of code on the screen and lots of deep conversation. Just how we like it for Going Deep and Expert to Expert.

Enjoy!

LOW RES FILE

MP4

ZUNE

Tags:

Follow the Discussion

  • Christian Liensbergerlittleguru <3 Seattle
    AWESOME! Thanks for this video, Charles. I love it already before having watched it *downloading*
  • CharlesCharles Welcome Change
    LOW RES FILE

    MP4

    ZUNE
  • Jonathan MerriweatherCyonix Me
    very cool, thanks for the video
  • stevo_stevo_ Human after all
    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..
  • CharlesCharles Welcome Change
    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.
  • Christian Liensbergerlittleguru <3 Seattle
    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 Sad
    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.
  • umer_aumer_a Mario be on XBOX one day.

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

  • Christian Liensbergerlittleguru <3 Seattle
    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...
  • umer_aumer_a Mario be on XBOX one day.
    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:

    win30 win30
  • Christian Liensbergerlittleguru <3 Seattle
    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 Perplexed 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.

  • umer_aumer_a Mario be on XBOX one day.
    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?


    Smiley 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.
  • Alexei PavlovBlackTiger If you stumbled and fell down, it doesn't mean yet, that you're going in the wrong direction.
    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... Cool
  • Christian Liensbergerlittleguru <3 Seattle
    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. Smiley

    But we are discussing things here that are only slightly related to the topic...
  • Vesuviusvesuvius Count Orlock
    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
  • Maddus MattusMaddus Mattus Maddus on C9, Is often ​controversi​al, But fun ​none-the-​less -​evildictait​or
    Very, very, very, very cool stuff!

    I would love to write software this way!

    You look nice in a suit Erik! Cool
  • Vesuviusvesuvius Count Orlock
    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#.

  • stevo_stevo_ Human after all
    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'..
  • Vesuviusvesuvius Count Orlock
    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.
  • stevo_stevo_ Human after all
    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.
  • William Staceystaceyw Before C# there was darkness...
    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.

Remove this comment

Remove this thread

close

Comments Closed

Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums,
or Contact Us and let us know.