A specification construction unit-based editor for Z

This paper proposes a formal specification supporting tool. It is designed on the basis of the specification reusability and the convenience to construct specification repository. The tool, called ZEditor, is designed for supporting the Z specification language. Two remarkable features of ZEditor are as follows. Firstly, we focus attention on some Z specification construction units so that ZEditor provides several specified input screens for them. Specifications described by ZEditor can be saved as the LATEX format or the XML one from each input screen. In each input screen, syntax and type checking of specifications can be also available. Secondly, the author can construct and edit an appropriate specification from some specification construction units which passed syntax and type checking. ZEditor will make it possible to describe specifications easily, to reuse correct specification construction units, and to support constructing specification repository.