Chapter in Software Specification Methods: An Overview Using a Case Study

I was asked to write a chapter for this book, which consists of a collection of formal specifications of the same example system written in a multitude of different formalisms. The system is so simple that the specification should be trivial in any sensible formalism. I bothered writing the chapter because it seemed like a good idea to have TLA+ represented in the book, and because it wasn’t much work since I was able to copy a lot from the Z specification in Jonathan Bowen’s chapter and simply explain how and why the Z and TLA+ specifications differ. Bowen’s chapter is available here.
Because the example is so simple and involves no concurrency, its TLA+ specification is neither interesting nor enlightening. However, my comments about the specification process may be of some interest.