Francesco Logozzo - Static Checking with Code Contracts for .NET
- Posted: Dec 22, 2009 at 11:47 AM
- 43,020 Views
- 4 Comments
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 WMV 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 WMV file.
- If you have a Zune, WP7, iPhone, iPad, or iPod 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…”
- MP3 (Audio only)
- MP4 (iPod, Zune HD)
- Mid Quality WMV (Lo-band, Mobile)
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.
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.
Follow the Discussion
Abstract interpretation and static checking is a real cool thing. Thanks for sharing this and keep pushing in further developments on this!
Cheers, Matthias
Great video and "promo"
I've just started using CC.
Thank you very much.
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?
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
Remove this comment
Remove this thread
close