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

  • Backend: Chalice
  • Language: Java
  • Features: Witnesses, Loop invariants
  • Path to Example File: witnesses/CounterState.java
  • Should Verify: Yes
  • Date: 2017-06-21
  • Lines of Code: 141 (comments not included)
  • Lines of Specification: 76 (53.9% of total)
  • Computation Time: 16.8 seconds