Manuel Fahndrich and Peli de Halleux - The Synergy of Code Contracts and Pex | Peli at RiSE

Manuel Fähndrich and Peli de Halleux sit down for a quick coding session that shows how to use Code Contracts and Pex together. Code Contracts can be used to specify what your code should do, they get turned into runtime checks which Pex can analyse and try to find counter-examples for. This was a fun session with Manuel and really shows the synergy of the two tools/approaches.

Both tools can be downloaded from Devlabs or our academic project pages.

Try it live at http://www.pexforfun.com
Code Contracts: http://research.microsoft.com/contracts
Pex: http://research.microsoft.com/pex
See this video in French!

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Follow the Discussion

Follow
Oops, something didn't work.

Try again?

Sign In to begin to follow these comments

What does this mean?
Following an item on Channel 9 allows you to watch for new content and comments that you are interested in. You need to be signed in to Channel 9 to use this feature.

Getting "follow" information

Stop following these comments

Start following these comments

What does this mean?
Following an item on Channel 9 allows you to watch for new content and comments that you are interested in and view them all on your notifications page.

Removing your "follow"

Setting up your "follow"

Did you know you can
sign up for email notifications?
- Subscribe to these comments

vesuvius Count Orlock

Apr 23, 2009 at 1:04 PM

I'm having problems downloading this (in that I cannot at the moment).

Anyone else have any joy?
aL_ Kinect ftw

Apr 23, 2009 at 2:14 PM

thats really cool
ive been using pex for a while and its really quite amazing how complex tests it can create
peli Peli

Apr 23, 2009 at 4:03 PM

Hi Vesuvius, there were some little errors in the URLs. Do you still have this problem?
vesuvius Count Orlock

Apr 23, 2009 at 11:58 PM

No, the problem is fixed now.

Thank you.

exoteric stuck in a loop, for a while

Apr 24, 2009 at 8:47 AM

It's quite nice to see this for .Net, especially with the smart code injection.

The embedded contract language is not as clean as in Eiffel, obviously

     put (x: ELEMENT; key: STRING) is
                     -- Insert x so that it will be retrievable through key.
             require
                     count <= capacity
                     not key.empty
             do
                     ... Some insertion algorithm ...
             ensure
                     has (x)
                     item (key) = x
                     count = old count + 1
             end

Also.  I don't quite agree that ensurances should come first (contrary to Eiffel), but granted, using the embedded technique where ther contracts are blended in with the rest of the code, it may be a better technique for readability. Maybe.

It's also striking how much use of contracts can be devoted to the type constraint for reference types that nullness not be part of the domain. How nice it would be with a simple language extension, even if only interpreted as a contract

     add (Point! x)

It's again the annoying wrong-default situation; as with of nullness over non-nullness there's also the variance over invariance (well, im/mutability if you will).

That Code contracts actually implements the old- and result-semantics is very nice.

Can we now expect .Net to be littered with Code Contracts all over for increased code correctness?

(oops, there goes the beautiful formatting heh)

MaF

Apr 24, 2009 at 2:05 PM

Sure, language syntax would be nice, but that's the language designers job. We've been there (Spec#), done that. We can only influence main stream languages so much. What we are doing now is providing mechanisms and tools without being language designers. Languages can then opt-in and provide whatever syntax they want.

The advantage to the programmer of course is that in the meantime, until language designers make up their mind, they can already work with this technology.
soum

Apr 24, 2009 at 6:56 PM

Does it work with the code contracts feature in .net 4.0?
peli Peli

Apr 24, 2009 at 8:19 PM

Yes - Code Contracts is the contract feature of .net 4.0 and Pex can already handle .net 4.0 processes. Since the Contracts API is still evolving there might be a difference between the .net 4.0 CTP release and the latest Code Contracts download (which Pex supports).

If you face any issues, don't hesitate to shoot emails in our forums at http://social.msdn.microsoft.com/Forums/en-US/category/devlabs
Charles Welcome Change

Apr 27, 2009 at 10:02 AM

It makes sense, in the context of .NET, that this tooling is designed to be language independent (just like .NET...). Why should every managed language have to provide the same internal semantics and language-appropriate syntax when a single shared library and IDE toolset gives all CLS compliant languages the same functionality for free? I think you guys are doing the right thing here.

Keep on pushing the envelope (independent of language design).
C