Comparison of the Z-Notation and Transition Specifications for Dynamic Abstract Data Types

Data Types Martin Große-Rhode Alfio Martini Technische Universitat Berlin, Fachbereich 13 Informatik, Franklinstrasse 28/29 D-10587 Berlin, Germany e-mail:fmgr,alfiog@cs.tu-berlin.de Abstract The Z-notation is a powerful tool for the formal specification of software systems, based on a model theoretic approach. Transition specifications are an extension of algebraic data type specifications to dynamic abstract data types, based on the idea of states as environments. Our aim in this paper is to define an (informal) translation between an algebraic core of the Z-notation and transition specifications. This allows to compare the approaches, relate their mutual benefits as well as to clarify how some main concepts -- locality, compositionality, and separation of concerns -- that are realized in transition specifications, could be carried over Z. 1 Introduction The Z--notation is an accepted and successful tool in the development of software systems. It is a language and style for the d..