#include "tree.h" /*@ requires valid_tree(t) @ ensures \result != \null => (path(t,\result) && \result->node == v) */ tree brute_force_search(tree t, int v) { tree u; if (t == NULL) return NULL; if (t->node == v) return t; u = brute_force_search(t->left, v); if (u != NULL) return u; return brute_force_search(t->right, v); } /*@ requires valid_tree(t) && bst(t) @ ensures \result != \null => (path(t,\result) && \result->node == v) */ tree binary_search(tree t, int v) { if (t == NULL) return NULL; if (t->node == v) return t; if (v < t->node) return binary_search(t->left, v); else return binary_search(t->right, v); } /*@ requires @ valid_tree(t) @ ensures @ \result => (bst(t) && \forall int x; in_tree(x, t) => min <= x <= max) @*/ int is_bst(tree t, int min, int max) { if (t == NULL) return 1; if (t->node < min || t->node > max) return 0; return (is_bst(t->left, min, t->node) && is_bst(t->right, t->node, max)); } /*@ requires valid_tree(t) @ ensures \result <=> heap(t) @*/ int is_heap(tree t) { if (t == NULL) return 1; if (t->left != NULL && t->left->node >= t->node) return 0; if (t->right != NULL && t->right->node >= t->node) return 0; return is_heap(t->left) && is_heap(t->right); }