Permissions: Bad loop (failing case 1)

Simple verification example case with permissions. A shared variable `val` is updated in a loop, but the order of the clauses in the loop invariant do matter here. This example is failing, since the `Perm(val,100)` invariant clause needs to be placed before the `val+tmp==\old(val)+n && tmp>0` clause.

General information

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

Statistical information

Lines of code16 lines (comments not included)
Lines of specification4 lines (25% of the total)
Computation time8266 milliseconds

Example code

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