Zeus:Zeus-Z

From Dependability

Zeus Project | Zeus-Z | Zeus-PVS | Related Sites | Related Publications

Screenshots | Downloads | Acknowledgements | Personnel


Zeus-Z uses Adobe FrameMaker™ connected to the theorem prover, Z/EVES™, developed by ORA Canada, to provide powerful support for specification development using the formal language, Z.

Through a simple system of menus and special windows, Zeus allows for easy development of both very large and very small specifications. It also has a windows interface to Z/EVES for syntax and type checking, which includes marking of the formal notation text that contain errors. A detailed description of Zeus-Z can be found by downloading the current version of the Zeus User's Manual.

Zeus-Z Toolset at a Glance

Features

  • WYSIWYG Editing of Natural Language and Z Notation
  • Checking of Natural Language
  • Checking of Z Notation
  • Importing and Exporting of LaTeX Representation of Z
  • Creating and Analyzing Domain Map
Retrieved from "http://dependability.cs.virginia.edu/info/Zeus:Zeus-Z"