Implementing and Combining Specifications

I wrote this note to help some Microsoft developers understand how they could write TLA+ specifications of the software they were designing. Their biggest problem was figuring out how to specify an API (Application Programming Interface) in TLA+, since there were no published examples of such specifications. The note also explains two other things they didn’t understand: what it means to implement an API specification and how to use an API specification in specifying a system that calls the API.