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

  • Backend: Chalice
  • Language: Java
  • Features: Sequences, Trees
  • Path to Example File: predicates/
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 42 (comments not included)
  • Lines of Specification: 19 (45.2% of total)
  • Computation Time: 6.9 seconds