Francesco Logozzo - Static Checking with Code Contracts for .NET

Sign in to queue

The Discussion

  • User profile image

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

    Cheers, Matthias

  • User profile image

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


    Thank you very much.

  • User profile image
    Andrew Zonov

    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?

  • User profile image

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



Add Your 2 Cents