specification sorts Tid; constants dummytid : Tid; comment: used to initialize the initial dummycell of the queue. Its value is irrelevant.; variables tid : Tid; end specification