Using Z specification, refinement and proof - Woodcock (Prentice Hall, 1996)