Channel 9

Entries:
Comments:
Posts:

Loading User Information from Channel 9

Something went wrong getting user information from Channel 9

MSDN

Activity Profile

Latest Achievement:

Loading User Information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements
Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

Research: Contract Checking and Automated Test Generation with Pex
Close

Download

How do I download the videos?

  • To download, right click the file type you would like and pick “Save target as…” or “Save link as…”

Why should I download videos from Channel9?

  • It's an easy way to save the videos you like locally.
  • You can save the videos in order to watch them offline.
  • If all you want is to hear the audio, you can download the MP3!

Which version should I choose?

  • If you want to view the video on your PC, Xbox or Media Center, download the High Quality MP4 file (this is the highest quality version we have available).
  • If you'd like a lower bitrate version, to reduce the download time or cost, then choose the Medium Quality MP4 file.
  • If you have a Windows Phone, iPhone, iPad, or Android device, choose the low or medium MP4 file.
  • If you just want to hear the audio of the video, choose the MP3 file.

Right click “Save as…”

  • MP4 (iPhone, Android)

    File size

    63.5 MB
  • Mid Quality WMV (Lo-band, Mobile)

    File size

    105.3 MB
  • WMV (WMV Video)

    File size

    299.2 MB
In theory, Design by Contract and unit testing are excellent approaches to improve code quality. Learn how to use code contracts that express pre-conditions, post-conditions, and object invariants in any managed language that improve testability, enhance static analysis, and serve as checked API documentation. Contracts are leveraged for advanced static analysis and translated into runtime checks. See how automated program exploration (Pex) discovers boundary conditions in code that cause failures and generates traditional unit test suites with high code coverage. Contracts and Pex work together to target contract checks, runtime failures (null dereferences, index out of range, etc.), and any other kind of assertions. Use them to write higher quality software with less effort.
  • Nikolai Tillmann
    Nikolai Tillmann has been with Microsoft Research for 6 years. He is currently leading the Pex project, building an automated test case generation tool for .NET based program analysis. Previously, he worked on Spec Explorer, a model-based testing tool.
  • Mike Barnett
    Mike Barnett has been at Microsoft Research since 1995. He has spent the last several years working on the Spec# project, an advanced verification environment and language for .NET.

Tags:

Follow the Discussion

  • Johannes HansenJohannesH
    Mike mentions that the current design by contract features are available for download under the research license. Where can I find that download?
  • simone_bsimone_b
    http://research.microsoft.com/research/downloads/details/4ed7dd5f-490b-489e-8ca8-109324279968/details.aspx
  • Judah Gabriel HimangoJudah

    Great stuff!

    I must admit I was saddened to hear Spec# wouldn't be integrated into C# 4. But this is the next best thing; I'm glad to see design-by-contract getting some attention in the .NET framework itself.

    If I may comment on the presentation, it feels like you both should have had your own presentations. It felt too rushed and too crammed.

    Having Mike go deeper into the evolution of Spec# and why they chose a library instead of C# langauge integration would've been great. And Nikolai covering more real-world unit testing scenarios with Pex - for example, testing code with dependencies like the file system or UI using Pex, would have been a great presentation by itself.

     Also, the rehearsed Q&A between Mike and Nikolai was cheesy. Too tongue-in-cheek! Smiley

    Beyond that, great stuff guys! I'm really happy to see DbC getting some real attention, I believe it will help us write code that more clearly expresses our intent and contains fewer bugs. That's something every developer can get behind. Going to go download and play with the VS2008-integration...

  • Judah Gabriel HimangoJudah
    After playing with the library for awhile, I think this has a lot of potentials.

    I'd like to give you guys some feedback as I considered how we would integrate this stuff into our codebase (that is, once contracts are under a commercial-friendly license!). Where do we send feedback?
  • Justin Van Patten - MSFTJustinVP
    Hi Judah, you can send feedback to bclpub@microsoft.com

    Cheers,

    Justin Van Patten
    Program Manager
    Common Language Runtime
  • dosborn278dosborn278
    The presentation was great and I love Pex and the contract stuff, but when are we going to get a license on it so that I can use it in vs2008 for the projects I am developing commerically, instead of just and academic license?
  • BradOBradO OSS Developer
    Agreed....Your Pex talk was one of the favorite I attended at PDC (despite the cheesy scripted dialogue - I didn't mind it  Smiley .  You guys did great breaking it down for people new to Design by Contract such as myself.

    But until this stuff is released under a non-research license, I just can't feel like I can use it and invest any time into it

    But great talk, great work on the technology...these are the things that excite me about where Microsoft is going
  • mbarnettmbarnett
    Thanks for all the great comments! I'm glad you pointed out our limitations as comedians: Nikolai and I had been just about to quit our day jobs and head back to LA to make our names in the comedy clubs there. I guess we'll just have to stay at MSR and work on Contracts and Pex!

    I just wanted to point out that we have a web site for the project: http://research.microsoft.com/contracts. That page contains a link to an email alias we've set up: codconfb _at_ microsoft _dot_ com. You can use that to send specific comments about the tools and the many bugs I'm sure you'll find in our tools. The alias is unfortunately one-way. We can see the mail you send to it, but you can't join the alias. We are working on a separate forum for the Code Contracts project, but it isn't set up yet.

    Mike
  • Jason BockJasonBock
    Mike,

    In the talk you mention that you do IL-weaving to inject the right code for the contracts. Is this IL reader/writer something that can be used separately from Contracts? I've been using Cecil (http://www.mono-project.com/cecil) for some R&D stuff and it would be awesome if there was something like this somewhere from Microsoft Smiley.

    Regards,
    Jason
  • Peli de Halleuxpeli Peli

    Pex is now available for Visual Studio 2008 under the pre-release license. Check it out at http://research.microsoft.com/pex/downloads.aspx .

  • Peli de Halleuxpeli Peli
    CCI (the framework used to rewrite the assemblies) was released as open source on codeplex at http://ccimetadata.codeplex.com.

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.

More entries in this blog

See More

Related entries

Creative Commons License

© 2014 Microsoft. Except where designated as licensed by
Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 License,
Microsoft reserves all rights associated with the materials on this site.