Permissions: Roster (fixed)

The verification example on page 42 of Clement Hurlin's PhD thesis. The example is a linked list representing grades (in a Roster). The roster has functionality to upgrade grades. We verify that these functions are correct.

General information

ID124
Articlenone
Back-endChalice
LanguageJava
FeaturesLists
Sources
Path to example filepermissions/RosterFixed.java
Date2017-06-20

Statistical information

Lines of code61 lines (comments not included)
Lines of specification23 lines (37.7% of the total)
Computation time8679 milliseconds

Example code

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