Loading User Information from Channel 9

Something went wrong getting user information from Channel 9

Latest Achievement:

Loading User Information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

Francesco Logozzo

Francesco Logozzo logozzo

Niner since 2010

  • Francesco Logozzo: Programmazione per Contratti e runtime checking in .NET con i CodeContracts


    In realta' l'ordine di valutazione e' ben preciso. Prima vengono valutate le precondizioni, poi il corpo del metodo, e quindi le postcondizioni. Quando fai l'override di un metodo, erediti anche la sua precondizione, che viene valutata prima dell'esecuzione del corpo del nuovo metodo, e la sua postcondizione, che viene valutata dopo. Il debugger ti permette di seguire la traccia d'esecuzione, e di vedere quale contratto e' violato. Nel mio esempio mi ha subito permesso di scoprire che la sottoclasse non si comporta "bene".



  • Francesco Logozzo - Static Checking with Code Contracts for .NET

    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.