Permissions: Binary search tree

Verifying a binary search tree with `del_min` operation. Note that only the access permissions are verified (implying that the program is memory safe). Functional properties are not yet checked.

General information

ID127
Articlenone
Back-endChalice
LanguageJava
FeaturesLoop invariants, Stacks, Trees
Sources
Path to example filepermissions/TreeStack.java
Date2017-06-20

Statistical information

Lines of code114 lines (comments not included)
Lines of specification47 lines (41.23% of the total)
Computation time13682 milliseconds

Example code

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