* Virtual Library * Formal Methods * Z Notation

Proposed extensions in HTML for Z

This document includes information on the display of the Z notation in World Wide Web pages and hyperlinks to related resources.

Note: The Z characters below will not display correctly on standard HTML browsers like Netscape although a number of ISO symbols are supported.


Mathematical extensions to HTML

This section summarizes early work undertaken by
Phillip M. Hallam-Baker at CERN on mathematical extensions to HTML including support for Z by WWW browsers.

Special Characters

The following characters are required to typeset Z but are not present in the HTML entity sets. Characters not present in the SGML ISO entity sets are marked *.

Free Types

[Name, Date]

Schemas

-------------------------
|AddBirthday
|Delta BirthdayBook
|name? : Name
|date? : Date
|---
|name? ∉ known
|birthday' = birthday ∪ {name ↦ date}
-------------------------

Generic Schemas

===[X,Y]=================
| _ ⊕ _ : (X ↛ Y) × (X ↛ Y) → (X ↛ Y)
|---
|∀ f, g: X ↛ Y •
|   f ⊕ g = ((dom g) &trianglerightbar; f) ∩ g
-------------------------

Axiomatic Descriptions

|Declaration
|--------
|Predicate


(La)TeX links

Of related interest: HyperTeX, a defacto standard for inclusion of hyperlink information in TeX (and LaTeX) documents.

Other links


Last updated 5 May 2002.

Page maintained by Jonathan Bowen.