Functional Verification

Functional Verification Goal

Verify real-world functional programs by specifying correctness properties and proving implementations satisfy them. Combines inductive types, recursive functions, and proof tactics.

Binary Search Tree Definition

Binary tree where each node's key > all keys in left subtree and < all keys in right subtree. Enables O(log n) lookup when balanced.

BST Lookup Specification

Requires two properties: (1) If element is in tree, lookup returns true. (2) If lookup returns true, element is in tree. Combined: lookup returns true iff element in tree.

Specification Completeness

Good specification must be precise and complete. Counterexample: lookup constant true satisfies first property but fails second; constant false fails first. Need both directions.

BST Assumption

Specification must assume tree is sorted. Unsorted tree breaks correctness of lookup algorithm. Precondition: t is a valid BST.

lookup Implementation

Recursively compare key: if n < node key, search left; if n > node key, search right; if equal, return true. Base case: empty tree returns false.

inversion Tactic

Used to reason about tree structure. From assumption that tree satisfies BST property, derives constraints on subtrees. Essential for proving lookup correctness.

Correctness Proof Structure

Induction on tree structure. Base case: empty tree, lookup false, element not in tree. Inductive case: assume property for subtrees, prove for node using BST ordering property.

Verified Functional Algorithms

Field of study developing provably correct implementations of classic algorithms (sorting, search, data structures). Combines programming language semantics with formal verification