Binary Search Trees

Viktor Kuncak 🌐

April 5, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The correctness is shown of binary search tree operations (lookup, insert and remove) implementing a set. Two versions are given, for both structured and linear (tactic-style) proofs. An implementation of integer-indexed maps is also verified.

License

BSD License

Topics

Session BinarySearchTree

Cite

× 
@article{BinarySearchTree-AFP,
  author  = {Viktor Kuncak},
  title   = {Binary Search Trees},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2004},
  note    = {\url{https://isa-afp.org/entries/BinarySearchTree.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: