This example shows a single-threaded Counter class with several methods (both static and dynamic) to increase the counter. We verify that the different ways to increase `val` are functionally correct and do not have races.
Path to example file
Lines of code
43 lines (comments not included)
Lines of specification
10 lines (23.26% of the total)
Note, verification may take a while and has a time-out of 20 seconds.