I think the author misunderstands. The spec is for a mutex, and it's written in an informal language, where the implementation fulfills a more formally expressed spec.