Francesco Logozzo - Static Checking with Code Contracts for .NET

Posted: Dec 22, 2009 at 11:47 AM

By: Peli de Halleux

(4)

43,733 Views

4 Comments

Video format

Option selected may change based on video formats available and browser capability.

Auto

Use our suggested format for this video.

Smooth Streaming

Adaptive bitrate streaming - little buffering but lower video quality at times of low bandwidth. Silverlight 5 required

Progressive

Traditional buffered video format. Silverlight 5 required

HTML5

For browsers that support H.264 MP4 or WebM video playback such as:
IE9+, Firefox 4+, Chrome 5+, or Safari 4+.

Flash

For browsers that have the Adobe Flash Player plugin installed.

Francesco Logozzo, a researcher at the Research in Software Engineering (RiSE) group at Microsoft Research, gives a demo of the Static Checker that comes with Code Contracts for .NET tools. The static checker allows you to verify that all the assertions in your code hold without actually running the code!

Francesco also goes to the whiteboard and gives us a short tutorial on Abstract Interpretation, the technique used by the static checker to prove the assertions.

Try the Code Contracts in your web browser at http://pex4fun.com/absverified!
Code Contracts Forums
Code Contracts Home page

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 be 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 this comments

minddriven.de

Dec 24, 2009 at 2:10 AM

Abstract interpretation and static checking is a real cool thing. Thanks for sharing this and keep pushing in further developments on this!

Cheers, Matthias
macias

Dec 29, 2009 at 4:16 AM

Great video and "promo" I've just started using CC.

Thank you very much.
Andrew Zonov

Jan 23, 2010 at 3:48 PM

Some remark, or maybe qestion about simple example on whiteboard... since we always entering that loop with x increment we should get postcondition of x > 0 strictly... why do all reasoning with intervals leads to x in [0, +inf] interval?
logozzo

Jan 28, 2010 at 1:05 PM

Hi Andrew,

that's a very good point.

(As far as x is concerned) the loop invariant is x >= 0, as before entering the loop x == 0, and then it is always incremented by one.

At the loop exit, we know that x >=0, but also that x > N (by the negation of the loop guard) and N > 0 (by the method precondition).

As a consequence we can refine the interval for x to [2, +oo].

I haven't mentioned it in the video to keep it simple, but you are right that the tool can prove a stronger assertion after the loop. In fact, if you download the checker, you can see that it proves the assertions x > 0 and x > 1 (but not x > 2 .

Thanks!

f