Permissions: Bad loop (failing case 2)

Simple verification example case where a shared variable `val` is updated inside a while-loop. This example fails, since the update to `val` can not be done: there is no permission to write to `val`.

General Information

  • Backend: Chalice
  • Language: Java
  • Features: Loop invariants
  • Path to Example File: permissions/
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 15 (comments not included)
  • Lines of Specification: 3 (20.0% of total)
  • Computation Time: 8.0 seconds