Verification of a Counter class that contains a single shared integer as field, and several methods that increase the counter in different ways. In particular, this verification example demonstrates the use of resource predicates and witnesses to do the verification.
Loop invariants, Witnesses
Path to example file
Lines of code
141 lines (comments not included)
Lines of specification
76 lines (53.9% of the total)
Note, verification may take a while and has a time-out of 20 seconds.