Abstract
Displaying the formal Z notation within a World Wide Web browser using standard HTML (HyperText Markup Language) pages is problematic because of the non-standard fonts used in Z, making it difficult to view Z documents on-line for some. This paper presents a solution to this problem. The formal text is formatted using a specially developed Java applet where the Z specification to be displayed is specified as a parameter to the applet, following the Z Interchange Format in the draft Z standard. A separate Java application program may be used to create and edit the Z specification. Other possible solutions and future directions are also discussed.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Adobe Systems Incorporated. PostScript Language Reference Manual, 2nd edn. Addison- Wesley Publishing Company, Reading (1990)
Berners-Lee, T.: World Wide Web past present and future. IEEE Computer 29(10), 69–77 (1996)
Bowen, J.P.: Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press (1996)
Bowen, J.P.: Proposed extensions in HTML for Z. Part of the Virtual Library, Zsection (1998), http://www.comlab.ox.ac.uk/archive/z/html-z.html
Bowen, J.P., Hinchey, M.G. (eds.): ZUM 1995. LNCS, vol. 967. Springer, Heidelberg (1995)
Brien, S.M., Nicholls, J.E.: Z base standard. Technical Monograph PRG-107, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK, (November 1992) Accepted for standardization under ISO/IEC JTC1/SC22
Chippington, D.: Presentation of Z specifications on the World Wide Web. Final Project Report 3/CS/6N – Computer Science Project, The University of Reading, Department of Computer Science, UK, May 5 (1998), http://www.fmse.cs.reading.ac.uk/z/java/report/
Ciancarini, P., Mascolo, C., Vitali, F.: Visualizing Z notation in HTML documents. In: P. Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 81–95. Springer, Heidelberg (1998) In this volume, http://www.cs.unibo.it/~fabio/displet.html
Dickie, G.A.: About IDVI, October 18 (1996), http://www.geom.umn.edu/java/idvi/
Drakos, N.: From text to hypertext: A post-hoc rationalisation of LATEX2HTML. In: Proc. 1st World Wide Web Conference, Geneva, Switzerland, CERN (May 1994), http://cbl.leeds.ac.uk/nikos/doc/www94/www94.html
Drakos, N.: The LATEX2HTML translator, February 23 (1998), http://www-dsed.llnl.gov/files/programs/unix/latex2html/
Flanagan, D.: Java in a Nutshell: A Desktop Quick Reference, 2nd edn. O’Reilly & Associates, Sebastopol (1997)
Flynn, P., et al.: Frequently Asked Questions about the Extensible Markup Language: The XML FAQ (1998), http://www.ucc.ie/xml/
Geometry Technologies, Inc. WebEQ: Putting math on the Web (1998), http://www.webeq.com/
Germán, D.M., Cowan, D.D.: Experiments with the Z Interchange Format and SGML. In: Bowen and Hinchey [5], pp. 224–233.
Yee, K.-P.: Mathematical expressions on the WWW (1996), http://www.lfw.org/math/
Lamport, L.: LATEX User’s Guide & Reference Manual: A document preparation system, 2nd edn. Addison-Wesley Publishing Company, Reading (1993)
Mikušiak, L., Adamy, M., Seidmann, T.: Publishing formal specifications in Z notation on the WWW. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 871–874. Springer, Heidelberg (1997)
Mikušiak, L., Vojtek, V., Hasaralejko, J., Hanzelová, J.: Z browser – tool for visualization of Z specifications. In: Bowen, Hinchey [5], pp. 510–523
Peeters, K.: nDVI: A DVI viewer plugin for Netscape (Unix) (October 8, 1997), http://norma.nikhef.nl/~t16/ndvidoc.html
Spivey, J.M.: The fuzz Manual. Computing Science Consultancy, 34 Westlands Grove, Stockton Lane, York YO3 0EF, UK, 2nd edition (July 1992)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)
World Wide Web Consortium (W3C). HTML 4.0 Specification, REC-html40-971218, W3C Recommendation (December 18 1997), http://www.w3.org/TR/REC-html40/
World Wide Web Consortium (W3C). Amaya – W3C’s browser/editor, July 10 (1998), http://www.w3.org/Amaya/
World Wide Web Consortium (W3C). Extensible Markup Language, XML (1998), http://www.w3.org/XML/
World Wide Web Consortium (W3C). HTML math overview (1998), http://www.w3.org/Math/
World Wide Web Consortium (W3C). Mathematical Markup Language (MathML), PR-math-19980224, W3C Proposed Recommendation (February 24, 1998), http://www.w3.org/TR/PR-math/
Jia, X.: ZTC: A Type Checker for Z – User’s Guide. Institute for Software Engineering, Department of Computer Science and Information Systems, DePaul University, Chicago, IL 60604, USA (1994)
Z Standard. Annex E – Interchange Format, Draft 1.2 (August 9, 1995), ftp://ftp.comlab.ox.ac.uk/pub/Zforum/ZSTAN/versions/part2.ps
Z Standard. Annex A – Lexis (December 1997), Draft 1.3. ftp://ftp.comlab.ox.ac.uk/pub/Zforum/ZSTAN/drafts/lexis.ps
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bowen, J.P., Chippington, D. (1998). Z on the Web Using Java. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive