From: narayana@oracorp.com
Newsgroups: comp.specification.z
Subject: Zed specification environment (product announcement)
Date: 26 Aug 92 14:42:11 GMT
X-Mailer: mail-news 2.0.3


\documentstyle[12pt]{article}
\begin{document}
\begin{center}
\Large 
Public Domain Product Announcement
\end{center}

We are pleased to announce the availability of ZED---a 
specification environment for the Z specification language.

ZED is an interactive and incremental environment for the 
Z specification language. The basic unit of editing in ZED 
is a paragraph which can be a schema, a definition, or an 
axiom, etc. An incremental parser permits the specification 
to be altered and the effects of changes in the specification 
to optimally propagate only to those attributes that are 
affected. This facility greatly reduces the computation 
overhead over batch mode environments. An incremental type 
inferencing algorithm provides for type-checking the 
specification.

ZED comes with a pleasant user-interface and a powerful set
of capabilities.  A WYSIWYG (What You See Is What You Get)
editor with graphical fonts allows the pleasant display of 
the paragraphs as they are typed. To permit documenting the 
specifications, ZED integrates \LaTeX\ and its previewers.
Menu based cut and paste facilities for fonts and for 
components of the specification enhance the power of ZED.

ZED directly supports many conventions adopted in industry
and academia in the use of the Z notation. An inheritance 
graph manager based on the inheritance relation between 
paragraphs maintains the specification as it is edited. 
A graph browser pretty displays the inheritance graph.

ZED is a X-window\footnote{X-Windows is a trademark of
the MIT X consortium.} based specification environment. It runs
on X v11 Release 5. X Toolkit and the Athena widget set 
are the artifacts used in building ZED.  ZED is customizable 
to any document preparation system. 

ZED accepts the Z notation as defined in the Z Reference
Manual. Since Z syntax has not been defined with mechanical
processing of specifications as a central concern, several 
engineering choices had to be made in building ZED. These 
choices contextually augment certain aspects of the Z 
notation to disambiguate the text. The User Manual for the 
ZED system records these facets and guides the user on 
constructing Z specifications using the system. 

ZED is a single-user specification environment written in
CWEB and is given as a front-end tool. Thus all its internal
data structures are completely accessible for any back-ends. 
In the current version, we have not provided any semantic 
support for refining Z specifications. Thus no automatic 
generation of proof obligations can be effected. Support for 
refinement and proof-checkers can form the backplane of the 
ZED environment.

ZED is intended to become a production quality environment. It
has been tested locally to the extent possible. However it
has not been tested in an industrial or academic environment
that extensively uses the Z notation. Thus we are making
available the current version of the system for alpha testing. 
We would like to hear from users about any bugs that they discover 
in the system.  We would like some sites to serve as alpha testing
sites so that we can bring the system to a stable state.
We hope to upgrade the system at various times. In such upgrades, 
user comments and experiences in the use of the system, and reporting 
of bugs will be extremely helpful.

Neither the authors of this software nor their affiliated
institutions are in any way legally liable for any deficiencies
encountered in the use of this software. This software is being
made available on an `as is where is basis' with no guarantees
to maintain the same. 


Enquiries about obtaining the ZED environment may be made to:
\begin{center}
Sanjeev Dharap\\
Department of Computer Science\\
Whitmore Laboratory\\
The Pennsylvania State University\\
University Park, Pa16802\\
Email: sanjeev@cs.psu.edu
\end{center}
or
\begin{center}
K.T. Narayana\\
ORA Corporation\\
301A Harris B Dates Drive\\
Ithaca, NY14850\\
Phone: 607-277-2020\\
Email: narayana@oracorp.com or narayana@cs.psu.edu
\end{center}
The second author gratefully acknowledges the partial
support by the Office of Naval Research under the grant 
number N00014-89-J-1171. Any opinions, findings, decisions, 
and conclusions contained in this announcement or in the 
software are those of the authors and not of the department 
of defense or the affiliated institutions of the authors.

Copy Rights: Parts of the ZED environment are built using GNU Bison 
software. In using or extending this software, the
copy right and licensing arrangements of Free Software Foundation 
shall apply.

\begin{flushleft}
~~~\\
~~~\\
Sanjeev Dharap\\
~\\
~\\
~\\
K.T. Narayana
\end{flushleft}

\end{document}