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

ID120
Articlenone
Back-endChalice
LanguageJava
FeaturesLoop invariants
Sources
Path to example filepermissions/BadLoop2.java
Date2017-06-20

Statistical information

Lines of code15 lines (comments not included)
Lines of specification3 lines (20% of the total)
Computation time8028 milliseconds

Example code

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