A GUI-based editor for checking and reusing Z specifications

It is problematic to describe the formal Z notation using a standard text editor. One of the reasons is to use the non-standard fonts and the special symbols in the Z notation, then making it difficult to write Z documents. This paper presents a solution to this problem. A prototype on GUI-based editor for Z specifications, named ZEditor, is developed and improved. Using ZEditor, Z documents are described as LATEX documents with the package for typesetting Z specifications. It is convenient to describe Z documents consist of many different components such as Axiom, Generic Constant, Basic Type, and Schema. Furthermore, it can save Z documents not only in LATEX form but also in XML one. The documents created by our system may be. used to create high quality documents, to browse on the Web, and to create specification repository for reuse.