Post-conditions and code lines for which all proof obligations have been proven are shown in green, as in the example line 123 below. Lines for which ESC Java still reports warnings are colored yellow, as in the example line 124. If a method does not contain any yellow lines, it is proven correct with respect to its specification. Click on the colored lines in the source code to inspect the warnings that ESC Java reports for them.
Loop headers are highlighted in blue, as shown in the example line below. Click on a loop header in the source code to view the loop invariants which Dynamate has produced for the loop.
125: while ( dummy <= 0 ) 