Predicates: Tree traversal

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.

General information

ID130
Articlenone
Back-endChalice
LanguageJava
FeaturesSequences, Trees
Sources
Path to example filepredicates/TreeRecursive.java
Date2017-06-20

Statistical information

Lines of code42 lines (comments not included)
Lines of specification19 lines (45.24% of the total)
Computation time6864 milliseconds

Example code

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