Calculating a Functional Module
for Binary Search Trees
Walter Dosch 1 and Bernhard Möller 2

1 Institut für Softwaretechnik und Programmiersprachen,
Medizinische Universität zu Lübeck, D--23538 Lübeck
2 Institut für Informatik, Universität Augsburg, D--86135 Augsburg

Abstract. We formally derive a functional module for binary search
trees comprising search, insert, delete, minimum and maximum opera-
tions. The derivation starts from an extensional specification that refers
only to the multiset of elements stored in the tree. The search tree prop-
erty is systematically derived as an implementation requirement.