this book reports on the design, implementation and evaluation of a new interactive z environment that is integrated into the eclipse environment. the z language is a formal specification notation that is used to describe and model computer-based systems.