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 using a binary search tree. In the case study, we’ll explore various considerations for writing a modular specification that encapsulates verfication details as well as implementation details.