@article{lamport2004implementing,
author = {Lamport, Leslie},
title = {Implementing and Combining Specifications},
year = {2004},
month = {September},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/implementing-combining-specifications/},
}