Temporal logic techniques have been proposed as a way of achieving a very natural transition from informal requirements to a formal specification of the requirements. The paper presents a case study of a real-life system developed using such techniques. Both a top-level specification and implementation semantics are given in temporal logic. In particular, the progression from statements in English to temporal logic is highlighted. A correctness proof that the implemented system satisfies the specification has been produced.