Witnesses: CounterState

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.

General information

ID161
Articlenone
Back-endChalice
LanguageJava
FeaturesLoop invariants, Witnesses
Sources
Path to example filewitnesses/CounterState.java
Date2017-06-21

Statistical information

Lines of code141 lines (comments not included)
Lines of specification76 lines (53.9% of the total)
Computation time16770 milliseconds

Example code

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