Reasoning in Z (PDF)
Reasoning in Z - episode 2 (PDF)
Z animation in Zans
See the "Allroutes" specification in Diller, Chap. 16.2
Allroutes improvments (PDF)
Using Z book
Chap. 22 -- Bounded Buffer