Writing and animating Z specifications. - Simon John Andrews (1996)