Verifying a container library #

In this section, we'll learn how to verify a simple container library, specifically, via an example of a map data structure implemented using a binary search tree. In the case study, we'll explore various considerations for writing a modular specification that encapsulates verification details as well as implementation details.