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/BadLoop2.java
• 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