The Bakery Algorithm: Yet Another Specification and Verification