History-based reasoning: loops
Verification example with history-based reasoning in which the actions in a loop are recorded. In particular, this verification example shows how histories are maintained in loop invariants.
|Path to example file||histories/HistoryLoop.java|
|Lines of code||41 lines (comments not included)|
|Lines of specification||18 lines (43.9% of the total)|
|Computation time||27045 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.