\documentclass{llncs}
\usepackage[dvips]{epsfig}
\usepackage{latexsym}
\usepackage{oz}

\begin{document}


%\newtheorem{theorem}{Theorem}
\newenvironment{display}{\par\begin{tabular}{l}}{\end{tabular}\par}
\newenvironment{boxdisplay}{\par\begin{tabular}{|l|}\hline}{\\\hline\end{tabular
}\par}

\newcommand{\uminus}{\cup \!\!\!\! \cdot \ }
\newcommand{\msetOpen}{\{ \! | }
\newcommand{\msetClos}{| \! \}}

%\title{Displaying notations in XML documents: the case for Z}
\title{Managing complex documents over the WWW: a case study for XML}

\author{Paolo Ciancarini, Fabio Vitali, Cecilia Mascolo}

\institute{Department of Computer Science,\\
University of Bologna,\\
Mura Anteo Zamboni ,7, I-40127 Bologna (Italy)\\
tel: +39 51 354506, fax: +39 51 354510\\
e-mail: {\tt \{ciancarini, vitali\}@cs.unibo.it}}
\maketitle

\begin{abstract}
The use of the WWW as a communication medium for knowledge engineers
and software designers is limited by the lack of tools for writing,
sharing, and verifying documents written with design notations.  For
instance, the Z language has a rich set of mathematical characters,
and requires graphic-rich boxes and schemas for structuring a
specification document.  It is difficult to integrate Z specifications
and text on WWW pages written with HTML, and traditional tools are not
suited for the task.

On the other hand, a new proposed standard for markup languages,
namely XML, allows one to define any set of markup elements,
hence it is suitable for describing any kind of notation.
Unfortunately, the proposed standard for rendering XML documents,
namely XSL, provides for text-only (although sophisticated) rendering
of XML documents, and thus it cannot be used for more complex notations.

We present a Java-based tool for applying any notation to elements of
XML documents. These XML documents can thus be shown on current
generation WWW browsers with Java capabilities. A complete package for
displaying Z specifications has been implemented and integrated with
standard text parts. Being a complete rendering engine, text parts and
Z specifications can be freely intermixed, and all the standard
features of XML (including HTML links, form elements, etc.) are
available outside and inside Z specifications. Furthermore, the
extensibility of our engine allows any additional notations to be
supported and integrated with the ones we describe here.

Keywords: document management systems, hypertext,
active documents, XML, Java, specification documents, Z notation.
\end{abstract}

\section{ Introduction}
\label{sec-intro}

In the last years, we have seen the WWW being slowly transformed from
an environment for sharing documents and data among members of
specialized communities (be they scientific, research, artistic,
social ones, etc.) to a general-purpose new medium for advertising and
marketing commercial enterprises to the public at large.  Since
commercial use has a larger impact and therefore power on the advances
of the medium, the specific needs of specialized communities have been
overlooked in the further development and advances of this new medium.

For instance, the use of the WWW as an environment for software design
introduces new problems and challenges:
the use of the WWW to support software process workflows,
sharing specification documents, allowing to read and write them, and
providing hypertextual links among documents is felt as a hot topic
\cite{KDJY97,ScaNol97}, but little specific aid to software designers
is available on the WWW at large.

A very important need that many communities of engineers have is the
support for special notations that are current or even absolutely
necessary within that community.  Currently the Web is very poor in
supporting special notations.  The typographical rendering of WWW
documents is usually defined using the HTML mark up language;
currently, it is the basis of most intranet document management systems
\cite{Ban97,Res97}. In its many versions, HTML provides textual support for
elements such
as input fields, buttons, choice lists, etc.  along with structural
and formatting commands for text within the data format of network
documents, and, of course, the hyperlinking capabilities that gave it
its name.

It has been extremely important that HTML allowed both complex
interfaces and proper and traditional text content to be described in
ASCII-based source documents. HTML has shown the way that text-based
support for non-textual content eases understanding, tool creation
and debugging of applications that deal with it. Furthermore, they
allow a complete intermix of different concerns, such as interface
elements and text characteristics, thereby fostering the creation of
complex interfaces that are at the same time rich in content and
sophisticated in their interaction with the user.

On the other hand, HTML is limited in that it has only a small set of
allowable elements, that is, only those that are explicitly defined in
the standard. Whenever some authors' needs exceed the capabilities of
the elements already defined in HTML, a different approach needs to be
used: either the existing tags are abused for a different purpose than
that for which they were designed, or an image is used, or a Java
applet is created providing the desired functionality.

These kludges have obvious and well known drawbacks, that have lead to
the development of many alternative (and partial) solutions. For
instance, Cascading Style Sheets (CSS, \cite{LieBos97}, \cite{BLLI98})
allow authors to
separate the efforts to specify special graphic effects and the
structure and determination of the actual content of the document,
allowing complex typographical rendering to be built on top of still
readable plain HTML documents.  XML \cite{BPSMQ97} is another
tentative in that direction: instead of forcing authors to the limited
and closed set of pre-defined elements, XML is a meta-markup language
that allow authors to define their own sets of markup elements that
are most appropriate to the specific class of documents they are
dealing with.  Adjunct languages (XSL, XPointer, XLink) are used by
authors to associate these elements to some rendering or linking
semantics for their display on paper or screen.  This allows a
definitive separation between the description of structures and roles
of the documents and the description of their graphical rendering on a
computer terminal or on a high resolution printer.

Neither solution is currently completely satisfying for supporting
specialized notations because both are only concerned with supporting
text-oriented content only. Many notations have sophisticated need that go
well beyond texts. For instance, specification languages like Z
\cite{Spi92} are often based on
specialized notations (mathematics and logic symbols): it would be
useful to be able to give a visual interpretation of these symbols and
to allow them to be displayed on WWW pages.

The purpose of this paper is to report on a Java rendering engine for
XML data that we have implemented. The engine allows standard typographical
support for text-oriented XML documents, as well as extensible graphical
support for additional needs, in particular for specialized notations.
We have created a complete graphical and typographical support for
formal specification documents written in Z.  The rendering engine we
are describing works as a completely autonomous applet inside unmodified
Java-enabled browsers such as Netscape Communicator or Microsoft
Internet Explorer.

The paper is structured as follows: in
section~\ref{sec-hyperZ} we summarize the state of the art
of the rendering of Z documents as hypertexts. In
section~\ref{sec-displets} we describe the idea of extending
HTML with Java using the {\it displets} concept.
Section~\ref{sec-engine} explains the implementation details
of our Z browser, whereas section~\ref{sec-browser}
describes the browser from the point of view of the author.
In section~\ref{sec-conc} we draw some conclusions and
sketch our future work.


\section{Creating Z specifications}
\label{sec-hyperZ}

\subsection{Writing, printing and visualizing Z specifications}
\label {ssec-printZ}

Several tools exist to this date to help software designers
to write, test, and share documents containing their Z specifications.
A complete guide to all the existing tools for Z can be found
in the site {\tt \small http://www.comlab.ox.ac.uk/archive/z.html}.

We can divide the available tools into four main categories:
fonts, browsers, editors, and type checkers.

True Type fonts for Z are available to use with common word processors on
many platforms including Windows and Macintosh, but fonts of course only
give access to the special mathematical characters of the Z language,
forcing users to use non-specific features of
available tools to create the
graphic boxes of schemata and other Z elements.

Customizable formatters such as LaTeX \cite{Lam86} are the most common
tools to write Z specifications. General style files for LaTeX, such as
{\tt oz.sty, fuzz.sty, ztc.sty}, have
been published to precisely render Z specifications.

Logica has created a syntax-driven WYSIWYG editor for Z on
MS Windows platforms.
Such an editor also integrates a type checker and forces
the production of well-formed Z specifications
by providing facilities for building, editing, checking,
and viewing Z specification documents.
Being WYSIWYG, the editor can display the Z constructs
and symbols as they would appear on a printed page.

The paper \cite{MVHH95} describes
the Z Browser, an application for displaying Z
specifications running on MS Windows.
Such a tool is aimed at Z novices, 
and is integrated with a complete help
system for Z grammar and notation,
thus it supports the construction,
syntactical check, and visual layout of Z documents.

Several analysis tools also exist for Z specifications.
For instance,
CadiZ \cite{Jor91} is an integrated suite of tools for
creating Z documents. It understands source files in LaTeX
and Word for Windows, and can visualize implicit Z expressions (i.e. schema
calculi) by showing their expansions.

Finally, the ZTC \cite{Xia94} type checker accepts LaTeX-formatted Z
specifications as well as text-based ones. ZTC also suggests
using a special syntax based on concatenation of
ASCII characters for mathematical symbols.

%F: Paragrafo nuovo
In summary, it is clear that Z is a highly structured notation
both graphically and semantically complex, 
and that writing, checking, and
displaying Z specification documents is yet an unsolved issue.

\subsection{Hypertext and Z specifications}

There are several good reasons to provide hypertext
functionalities to Z specifications. A complex specification
is intrinsically composed of many connected chunks (schemas,
etc.) that refer to each other in a peculiar, often
unpredictable way. Furthermore, the idea of literate
programming \cite{Knu84} requires that schemas and texts
interleave freely, so that the reader is provided with a
narrative explanation of the most complex schemas, and a
formalized and exact specification of vaguer descriptions.
These remarks naturally call for a hypertext solution.

Moreover, collaboration and sharing are even better reasons
for providing hypertext support to Z specifications: formal
specifications are but one step in the complex process of
system design, verification, and implementation
\cite{FKV94}. Modern development processes are enacted by
teams of people that cooperate, interact, and discuss. Being
able to create, access, and verify formal specifications
within the usual tools of our everyday work, publish them,
connect them to the other deliverables of the design and
implementation processes would allow a tighter integration
between formal design and actual implementation
\cite{CFR97}.

Till recently, Z specifications could only be visualized on the WWW by
creating images in one of the supported inline formats, such as GIF. This
leads to a very cumbersome and unnatural creation process, since the Z
specifications have to be created in a different environment than the text,
and furthermore non-specialized graphic editors have to be used and
restrained in order to produce graphically acceptable schemas. It is also a
very unnatural and clumsy way of accessing to the information: an image of
a schema is a completely opaque object, where the subparts, the texts, the
formulas are completely inaccessible; it is a bitmap that cannot be further
processed because the content and meaning have been lost: the content of a
schema cannot be searched, the specifications cannot be indexed, analyzed
or verified.

A first attempt to show Z specifications on the WWW was
described in \cite{MAS97}, designing
a plug-in for Netscape and Internet Explorer that accepts Z
specifications written using one of the existing LaTeX styles.

Although this approach is very original it has two main limitations: first,
visualizing Z documents requires the availability of the plug-in, which is
architecture-dependent (it only exists for MS Windows).
Secondly, the LaTeX format is alien
to the available SGML-based formats
suggested for the WWW:
in fact, writing Z schemas in LaTeX requires a different
syntax and approach than writing the surrounding free-flow text in HTML,
and the specifications live independently of the host document.
The first problem has been addressed: the Z browser is
becoming a Java applet, which is architecture-independent and can be run on
most computers of the current generation.

We know that also J. Bowen and others in Reading are working
on a Java applet to visualize Z schemas \cite{BowChi98}.
Our approach, detailed in section
\ref{sec-browser}, is related but with relevant differences.

\subsection {The advantages of markup languages}
\label{ssec-markup}

HTML has been extremely successful in allowing unsophisticated
network users to become authors of fairly complex documents, even
in the absence of widespread editing tools. Nonetheless, there
has been in the past two or three years a widespread awareness
(\cite{SMG94}) that HTML has reached its potential, and
that a change of paradigm was necessary.

The major drawback of HTML is that it allows only a
pre-specified set of elements. Authors can only use these
elements, and have to limit their authoring needs to what is
available within the existing language, or to force these
elements beyond their intended meaning.

HTML is an application of the Standard Generalized Markup
Language \cite{SMG94}, that is, a class of documents conforming to the
SGML Document Type Definition (DTD) that describes ``HTML
documents''.
SGML, being a meta-language describing
classes of documents rather than one specific class, is free of
the above mentioned limitations of HTML: by appropriately
creating a custom class of documents, and defining the legal
elements therein, authors can provide support for any kind of
rhetoric need, however complex and arcane.

Unfortunately, SGML is considerably more complex to learn
and design documents with than HTML, and it has been felt
that this would prevent its generalized adoption. Therefore
the SGML working group of the Word Wide Web Consortium was
asked to develop a new mark-up meta-language, namely the
Extensible Markup Language (XML) \cite{BPSMQ97}, to take the
place of SGML on the Web. XML documents would have to be
straightforwardly usable over the Internet, compatible with
SGML, and easy to create.

%F Nuovo paragrafo
There are several standards being developed within the XML
framework: the most important is XML itself, a meta-markup
language that allows user to create their own set of
elements for their class of documents. XPointer and Xlink
(\cite{MDR98a} and \cite{MDR98b}) extend HTML linking mechanism by providing
external specifications of locations, multiple links,
external links, etc. XSL \cite{CD98} associates rendering
behavior (e.g. character and paragraph settings) to XML
elements through a mapping and rewriting language.
XML-Namespace \cite{BHL98} allows elements coming from
different namespaces (document types, for instance) to live
together in the same document. Very important is MathML
\cite{IM98}, a markup language for mathematics, formerly part
of the unborn HTML 3.0 and subsequently detached in an
autonomous standard finally converted into XML. MathML
covers most needs for mathematical rendering, and is capable
of showing most of the strange glyphs that are part of the Z
language, but is not thought for Z and does not provide
support for other, more specific needs of the Z notation.

Interestingly,
in the Z community an SGML-based language for Z specifications
already exists: the Z Interchange Format (ZIF for short)
\cite{BriNic92} defines a portable representation of Z, that can be
used by all tools supporting SGML.
The ZIF is basically a
Document Type Definition (DTD), namely an SGML specification defining
the syntax of documents that contain Z specifications.
In \cite{GerCow95} a study of the usage of the ZIF was
presented, according to which ZIF can be fruitfully used to
create editors for Z documents using standard SGML tools, and
that Z specifications encoded using ZIF could easily be included
in other SGML documents.

XML documents are valid SGML documents. Most existing SGML
DTDs can be used with no modifications in an XML
environment. Notably, the Z Interchange Format is one of
such DTDs.

It is therefore possible to use the definitions specified in the
ZIF within XML tools, in order to create web-friendly visualizations of Z
specifications.
Alternatively, XML tools allow the HTML tag set to be
described and extended as needed. By joining the HTML DTD with the ZIF DTD,
and producing a capable browser, it is possible to write HTML documents
that contain Z specifications as markup items, instead of images, thereby
keeping all the useful properties that markup has over bitmaps.

In this paper we report about one such tool, that allow the display of
text-based XML documents enriched with Z specifications. This mechanism can
obviously be extended to handle the display of any kind of notation within
a XML document.

\section{Displets and markup languages}
\label{sec-displets}

{\it Displets} were proposed in \cite{VCB97} as a way to extend
HTML documents using Java. The HTML language was extended on a
per-document basis by defining new tags as needed, and providing
Java classes to take care of their graphical display. While not
providing all the functionality and flexibility of a full
meta-mark up language such as XML (Sect.~\ref{sec-hyperZ}),
HTML extended with
displets could allow all kinds of specialized notations and
graphical effects while at the same time leveraging over the
existing and well-known set of elements defined by HTML.

Our first experiment with rendering arbitrary, non-text-based
mark up extensions \cite{VCB97} was to modify an existing browser to
allow the parsing and the visualization of new HTML-like
elements. To do so, we took an early version of the HotJava
browser, whose source code was freely available, and modified it
so that it could accept on-the-fly extensions of the HTML DTD and
load the appropriate classes (called {\it displets}) whenever
the newly defined tags were to be displayed. That experiment was
extremely limited, in that we used an old version of the Java
language, and worked only on a specific version of a specific
browser. Furthermore, we heavily relied on the existing rendering
architecture of the browser and just provided a minimal effort
implementation (basically a displet was just a sequence of
drawing instructions for the visualization of the elements).

In \cite{CRV98a}, on the other hand, we reported about the
DispletManager applet, a general, extensible rendering and
architecture we have been working on, which can be used
for both extensions to HTML and straight XML documents. This
architecture is embodied in a Java applet that can be run within
any Java-enabled browser such as Netscape Communicator or MS
Internet Explorer.

Fundamental design requirements for the rendering engine have been:

\begin{itemize}
\item
    it must be possible to create special code for rendering
        arbitrarily odd data types, in particular non-textual
        data ({\it displets}).
\item all displets must easily integrate with each other: a
        chart element may have a mathematical formula as one of
        the labels, and some staff notation as another, where
        some notes may act as hypertext links.
\item the rendering engine must work both for extended HTML and
        for straight XML, and the displet classes must be
        identical.
\end{itemize}

Figure \ref{fig-displet}  shows the general structure of the DispletManager
applet:


\begin{figure}[htp]
\centerline{\scalebox{0.60}{ \epsfbox{./fig1.epsf} } }
\caption{The general structure of the DispletManager applet}
\label{fig-displet}
\end{figure}


The document chunk to be displayed, be it HTML or XML, is
loaded by the displet manager and parsed by the appropriate
parser. The resulting tree is then recursively (depth-first)
analyzed: the appropriate displet classes are activated to create
the rendering (i.e., the display object) of their element on the basis of
the rendering of their sub-elements.
No class is allowed direct access to the
screen: on the contrary, each displet creates a (set of) off-screen
bitmap(s) that its ancestor can pass, ignore, modify or add to.

%F: Nuovo paragrafo
Several specialized browsers exist for XML-based special
notations. For instance, WebEQ for MathML \cite{webeq} and Jumbo
for CML, a XML-based notation for chemical data \cite{jumbo}.
Although a specialized browser would have probably been more
efficient and sophisticated for Z elements, too, we felt
that a general rendering engines for all kinds of notation
was preferred, leading us to a more general and extensible
architecture for Z and other needs.

\subsection{Applying displets to XML documents}
\label{ssec-extending}

The XML language allows authors to define their own set of elements (tags)
to structure and organize their documents. Of course these elements do not
have a pre-defined meaning, nor even a pre-defined visualization. For
instance, while it is known that the "H1" element in HTML has both a
structural role (the heading of a first level section) and a graphical
rendering (use a large font and align it on the left), a corresponding
"major-heading" element in a XML document would have no
machine-understandable structural role (but this is not a problem), nor a
known graphical rendering (we can not even determine whether the element is
a block, a paragraph or an inline element).

The XSL \cite{CD98} language is used for associating
rendering information to an XML document.  Each XML document that needs
to be displayed on screen or on a printer would have a XSL document
associated.  The XSL document contains a series of "rules" mapping the XML
elements of the document to one or more {\it flow objects}
(i.e., graphical objects such as blocks, paragraphs and inline texts).

%F: Nuovo paragrafo
There are two competing syntax for XSL stylesheets: the
first is based on a very early proposal for XML stylesheets
\cite{ABC97}, and is the one implemented on most applications
and discussed in most books about XML (for instance,
\cite{Hol98}). The second one, a W3C Recommendation, came out
recently (August 1998, \cite{CD98}) and still very little
support can be found for it. Our terminology, discussion and
implementation relies still on the first version.

Although in XSL the set of available flow objects is fixed, we allow the
specification of new flow objects, that can be specified in the rules
just like the standard ones.  Each flow object corresponds directly to
a displet class.

What follows is an example of a simple XML document contained in the
DispletManager applet and its associated XSL style rules.  The style
sheet refers to two flow objects: a standard paragraph object
(belonging to the CSS family of flow objects available within the
standard XSL proposal), and a special "reverse" flow object that is
prepared as a displet by the author of the document:

\begin{verbatim}
<applet code="DispletManager.class" width=500 height=200>
<param name = "style" value = "

<xsl>
<rule>
        <target-element value='para'/>
        <css.div font-size='12'>
                <children/>
        </css.div>
</rule>

<rule>
        <target-element value='rev'/>
        <example.reverse>
                <children/>
        </example.reverse>
</rule>

</xsl>  ">

<param name = "XMLcode" value="

<para>This is an example of a text rendered in
<rev>reverse</rev></para>

">
</applet>
\end{verbatim}

The DispletManager applet for XML has two arguments: the first contains
the style sheet document according to the XSL rules, while the
second one contains the XML document that has to be displayed, using the
elements that are described in the XSL style sheet associated.

Upon loading the applet, the displet manager will start the XSL engine and
read in the 'style' parameter. This is parsed (by a XML parser, because it
is itself a XML document) and organized. Then the XMLcode parameter is read
and parsed by the same XML parser, creating a tree of elements and data.

The XSL engine will then match each element in the XML document with the
{\it pattern} contained in each XSL rule. When the most suitable match has
been found, the rest of the rule (the {\it action} part) is executed,
creating the flow objects listed and feeding them their content (usually
the rendering of their subelements, as specified by the $<children/>$ tag).

In this example, the 'para' element of the XML document matches the first
XSL rule, triggering the creation of a 'div' object of the standard CSS
package (a paragraph) with a specific parameter (font-size=12), fed with
the children of the element (i.e., the words and the elements contained
within the para tags). Then the 'rev' element is considered, and matched to
the second rule of the stylesheet, triggering the creation of a 'reverse'
object belonging to the 'example' package, fed with its content. As soon as
the rendering of its content has been readied (by creating the necessary
bitmaps), the displet class corresponding to the flow object is activated.

Each displet will then produce a
(list of) bitmaps of its content.  
For instance, the 'div' displet of the
CSS package will set a few parameters 
(such as margins, line spacing, font, and size) 
that may affect its sub-elements, wait for the XSL engine to return
control after its content has been readied, and build its own content by
combining the bitmaps of each word into lines according to the given
constraints. Figure \ref{fig-render} shows the above mentioned document
results on screen:

\begin{figure}[htp]
\centerline{\scalebox{0.60}{ \epsfbox{./fig2.epsf} } }
\caption{Rendering a simple displet}
\label{fig-render}
\end{figure}

\section{The rendering engine}
\label{sec-engine}

The rendering engine used by the DispletManager applet
consists of a set of Java classes that provide the rendering for the
appropriate document elements.
These classes are all subclasses of the DocElement class,
which provides the framework of the rendering procedure.

All classes provide a {\tt createBitmap()} method, whose purpose is
to create and return the bitmap of the flow object of the
considered mark up element on the basis of the bitmaps of its
sub-elements. The {\tt createBitmap()} method is usually not seen by
the implementer of new classes, and provides the following
functionalities:

\begin{itemize}
\item
    an active drawing environment is managed. The drawing
        environment is a set of parameters that are used by the
        rendering methods of the classes in order to decide how
        to create the bitmaps. For instance, a paragraph-like
        class may set some parameters that will be used by
        itself, such as margins, line spacing, alignment, etc.,
        and some that will be used by its sub-elements, such as
        font name, font size, font color, etc. The
        {\tt createBitmap()} method allows a displet to set its own
        attributes with the {\tt setParams()} method, and restores the
        previous situation when the displet is finished. Since
        {\tt createBitmap()} methods are recursively activated, this
        creates a stack that provides the proper parameters at
        any level of recursion.
\item the rendering of sub-elements is managed. The
        presence/absence of the element in the XSL rule may cause or
        prevent the rendering of the sub-elements of the current
        element.
\item the rendering of the element is managed. After the
        bitmaps of the sub-elements of the element have been
        created (if appropriate), the {\tt createBitmap()} method calls
        the {\tt render()} method, which in turn
        creates the final bitmap (or
        set of bitmaps) that will be returned. Different classes
        will implement {\tt render()} differently: for instance, the
        {\tt render()} method of a block element will collect the
        bitmaps of its sub-elements in a vertical stack (one
        above the other), and provide a single bitmap of the
        whole element, while the {\tt render()} method of a paragraph
        will collect its sub-elements side-by-side in lines of
        the given width, and provide a bitmap for every line it
        has created; this allow the element containing the
        paragraph to decide how much of the paragraph to display
        at a time (for instance, in case of scrolling).
\item active elements are specified and created. Active
        elements are those that will need to react to user and
        system events after they have been displayed. For
        instance, form elements and anchors have an associated
        behavior that is activated when the user selects them.
\end{itemize}

Figure \ref{fig-inherit} shows the inheritance structure of the classes of the
module library:

\begin{figure}[htp]
\centerline{\scalebox{0.60}{ \epsfbox{./fig3.epsf} } }
\caption{The inheritance structure of the module library}
\label{fig-inherit}
\end{figure}


DocElements can either be data, entities or tag elements.
DataElement classes are used for the content of mark up elements,
i.e., \#PCDATA in SGML and XML DTDs. They can either be text or
hidden elements. EntityElements are provided for the management
of XML and HTML entities such as \&amp; or the definition of
new ones. TagElements are used for the creation of the structure
flow objects of the document: they are either flow objects, block
objects, inline elements or special elements.

\begin{itemize}
\item
    A block element is a single object that stands alone in
        the vertical layout of the document. Paragraphs or tables
        are block elements. A flow element is a block element
        that is built piecemeal: while plain block elements are
        built from start to end before the {\tt createBitmap()}
        returns, flow elements build each of their sub-element
        and return, and are called as many times as there are
        sub-elements. This allows long and complex elements to be
        rendered only for the possibly small section that is
        actually displayed. For instance, HTML and BODY are
        considered flow elements, so that the display of an HTML
        document can start as soon as the first object is
        completed, and be interrupted when the available display
        space is filled.
\item Inline elements are elements that can be put side by side
        with their siblings. Inline elements are used within
        block elements and may be text-based, images or something
        else. The StyledText class allows the specification of
        text runs of arbitrary styles. Inline elements specify
        the places where they can be broken by creating as many
        bitmaps as break points. This allows the containing
        paragraph or block element to determine where the line
        should be broken.
\item Special elements are completely tailorable. While in the
        previous classes displet programmers can only overload
        the {\tt setParams()} and {\tt render()} methods, here all methods
        are overloadable, and can be customized.
\end{itemize}

As an example, this is the complete source code of the
'reverse' displet:

\begin{verbatim}
package example;
import displet.*;

public class reverse extends StyledText {
        public void setParams(StyledTextParams p) {
                Color c = p.fgColor;
                p.fgColor = p.bgColor ;
                p.bgColor = c ;
        }
}
\end{verbatim}

The reverse displet is a subclass of the StyledText, which is
a subclass of the InlineElement class. These are classes for
text-based objects that behave as in-line elements (eg. bold,
italic, etc.). As it can be seen, the programmer of such a
displet only has had to specify a parameter
and have the {\tt render()}
method of its superclass handle all the details. The
displets for showing Z specifications are shown in the following section.

\section{The Z browser}
\label{sec-browser}

The main extension to HTML we have considered using displets is the
implementation of the complete ZIF DTD. Authors writing Z specifications
can create documents containing their Z specifications in a markup language
similar to HTML and completely intermixable with plain text and other HTML
features such as links, tables, etc.

The ZIF format defines several elements (tags) for the building blocks of
the language, such as schemas, definitions, etc., and several entities
(literal macros) for the special characters inherited from mathematics and
logics. Each element is implemented by a displet that creates a bitmap
where the content of the element is appropriately composed and the
graphical elements such as boxes, lines, etc. are then added. Entities on
the other hand are elements of a graphical alphabet that is contained in a
single GIF image and is loaded with the displets.

The following is an example of a Z schema using the Z Interchange format:

\begin{verbatim}
<givendef>
    NAME, DATE
</givendef>
<schemadef>
    BirthdayBook
    <decpart>
        <declaration> known: &pset; NAME</declaration>
        <declaration> birthday: NAME &pfun; DATE </declaration>
    </decpart>
    <axpart>
        <predicate>known = &dom; birthday</predicate>
    </axpart>
</schemadef>
\end{verbatim}

A schema is defined by a tag called schemadef, which contains three
elements: the name of the schema, a declaration part and an axiom part. The
declaration part contains one or more declarations, and the axiom part
contains zero or more predicates. Appropriate ordering and nesting of
elements is enforced by the DTD, and is checked when parsing the document.
The notations ``\&pset;'', ``\&pfun;'' and ``\&dom;'' are three entities
(respectively, the partial set symbol, the partial function symbol and the
domain symbol) that will be substituted by the corresponding element in the
graphical alphabet containing all the relevant Z symbols. The displet
manager can appropriately show document bits as the previous one in a WWW
browser.

Since many Z specifiers use LaTeX to produce their Z documents,
we have developed an off-line translator called ``Zed2XML'' that
transforms Z specifications written in LaTeX using style {\tt oz.tex}
into a corresponding HTML document with the appropriate extension.

For instance, given the following Z specification (the basic birthday
book example from \cite{Spi92}):
\begin{zed}
[NAME, DATE]
\end{zed}

\begin{schema}{BirthdayBook}
known: \power NAME\\
birthday: NAME \pfun DATE
\where
known = \dom birthday
\end{schema}

corresponding to the following LaTeX source document:

{\small

\begin{verbatim}
\documentclass[italian,12pt,twoside,openright]{report}
\usepackage{amsfonts}
\usepackage{oz}

\begin{document}

\begin{zed}
[NAME, DATE]
\end{zed}

\begin{schema}{BirthdayBook}
known: \power NAME\\
birthday: NAME \pfun DATE
\where
known = \dom birthday
\end{schema}
\end{document}
\end{verbatim}

}

The Zed2XML application transforms the previous LaTeX example in the
corresponding applet specification:

{\small
\begin{verbatim}

<applet  archive="displet.zip" code="XMLManager.class"  width=450 height=200>
<param name = "XMLcode" value="

<givendef>
    <a name="name">NAME</a>,
    <a name="date">DATE</a>
</givendef>
<schemadef>
    BirthdayBook
    <decpart>
        <declaration>
            known: pset; <a href="#name">NAME</a>
        </declaration>
        <declaration>
            birthday: <a href="#name">NAME</a> pfun;<a href="#date"> DATE</a>
        </declaration>
    </decpart>
    <axpart>
        <predicate>
            known = dom; birthday
        </predicate>
    </axpart>
</schemadef>

"> <param name = "style" value="
<xsl>
    <import name="htmlcss.stl"/>
    <import name="Zpackage.stl"/>
</xsl>

"></applet>
\end{verbatim}

}

The output of Zed2XML is the HTML specification of the {\em DispletManager}
applet. As it can be seen, we are following the ZIF format quite strictly.
For the sake of brevity and reusability, standard stylesheets are used and
invoked by a simple import command in the specification of the applet.

The 'htmlcss.stl' document contains the XSL rules to use HTML elements
within XML documents. For instance, we are using here HTML links with the A
tag. This is the relevant excerpt from the 'htmlcss.stl' document:

\begin{verbatim}
<rule>
    <target-element type="a">
        <attribute name="href" value="%2"/>
    </target-element>
    <css.a href="%2">
        <children/>
    </css.a>
</rule>
\end{verbatim}

The 'Zpackage.xsl' document contains the XSL rules to use the Z displets
within XML documents. This is an excerpt from this stylesheet:

\begin{verbatim}
<rule>
    <target-element type="givendef"/>
    <zpack.givendef>
        <children/>
    </zpack.givendef>
</rule>

<rule>
    <target-element type="schemadef">
    <zpack.schemadef>
        <children/>
    </zpack.schemadef>
</rule>
\end{verbatim}

When run on a WWW browser, the previous documents is shown as in figure
\ref{fig-imple}.

\begin{figure}[htp]
\centerline{\scalebox{0.60}{ \epsfbox{./fig4.epsf} } }
\caption{Visualization on the WWW of a Z schema}
\label{fig-imple}
\end{figure}

We remark that all displets integrate with each other and can refer to each
other freely.  In our case, the Z schema contains a hypertext link
described in a different package. Z elements and plain text based XML
elements freely intermix: it is possible to put standard HTML tags
within Z schemas, for instance an author may require that some
declarations of a schema are written in bold.  The Zed2XML translator
automatically connects types used in declarations to their definitions
using plain HTML links.  The author may freely add or modify the
available links and HTML features, and include additional HTML
elements, as well as native XML elements or elements belonging from
other packages of displets.


\section{Conclusions}
\label{sec-conc}

We have presented a tool for visualizing Z specifications on
the WWW: it fits every browser and every platform.
The tool is based on XML displayed through ``displets''.

The advantage of having a Z browser running on all platforms is
essentially that sharing of Z documents is encouraged by the diffusion
of WWW on the Internet.

A possible application can be a groupware tool
for editing and versioning formal documents; such a tool
could be integrated with other software tools in
order to improve the specification phase of the software process.

The reuse of parts of documents obviously benefits from having
these hypertextual Z documents. The tools will also improve the
search of pieces of specifications in complex documents: every
element in the Z specification can be labeled or linked to other
pieces of documents or to URL on the Internet.

XML can be further extended in order to
include new symbols and integrate Z specification with other
notations: new Java classes have to be written for the new symbols.

Our most ambitious goal consists of defining all XML displets
necessary in an organization to support the intranet
management system of formal documents typical of such an organization.
For instance, we are currently working on displets for
managing UML documents.

A displet site is available at

{\tt http://www.cs.unibo.it/\char126fabio/displet.html}.

This site contains the code for the rendering engines,
examples for both HTML and XML,
and a list of all the displets we have created so far.

{\bf Acknowledgments:}
We would like to acknowledge the help and contribution of
our students Alfredo Rizzi and Stefano Pancaldi, 
and the help and suggestions of 
Michael Bieber and Chao-Min Chiu. 
We also would like to thanks our anonymous
reviewers for their helpful comments and suggestions 
on both the paper and the project itself.

\bibliographystyle{abbrv}
\bibliography{biblio}

\end{document}
}


