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.
|Features||Loop invariants, Stacks, Trees|
|Path to example file||permissions/TreeStack.java|
|Lines of code||114 lines (comments not included)|
|Lines of specification||47 lines (41.23% of the total)|
|Computation time||13682 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.