Using Z : specification, refinement, and proof / Jim Woodcock and Jim Davies. - Woodcock, Jim (Prentice Hall international series in computer science, 1996)