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.

General information

ID73
Articlenone
Back-endSilicon
LanguageJava
FeaturesHistories
Sources
Path to example filehistories/HistoryLoop.java
Date2017-06-19

Statistical information

Lines of code41 lines (comments not included)
Lines of specification18 lines (43.9% of the total)
Computation time27045 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.