Witnesses: Recursive tree 3 (magic wand)
This file demonstrates how a magic wand can be used to prove that the deletion of a node from a binary search tree is sound.
|Features||Magic wands, Sequences, Trees, Witnesses|
|Path to example file||witnesses/TreeWandSilver.java|
|Lines of code||101 lines (comments not included)|
|Lines of specification||67 lines (66.34% of the total)|
|Computation time||78023 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.