A tree data structure implemented in Java, together with a recursive method `del_min` that deletes the smallest value from the tree. The state of the tree is represented as a `state()` predicate. We verify that `del_min` is correct.
Path to example file
Lines of code
42 lines (comments not included)
Lines of specification
19 lines (45.24% of the total)
Note, verification may take a while and has a time-out of 20 seconds.