TOZE, a graphical editor for the object-Z specification language with syntax and type checking capabilities

Abstract

This manuscript describes the development of a tool that allows users to create and edit formal specifications in the Object-Z language using a graphical user interface. The tool enables users to enter Object-Z specifications, validate correctness of the syntax, and check for type inconsistencies. The vision for the editor was to make it work similar to a WYSIWYG word processor, like Word, where the user is able to work with the content as it would appear on a printed page. Unlike other tools for Object-Z, TOZE provides interactive facilities to check syntax and types within the tool without the need to leave the editor and use other applications. Basic file management functionalities such as saving and opening specifications as well as more advanced features such as exporting the specification as a JPEG image or LaTeX document are provided.