文法や型のチェッカや LaTeX のスタイルファイルやフォントなどのパッケー ジであるfuzz はSpivey Partnership, 10 Warneford Road, Oxford OX4 1LU, UKから手に入れることができます.これは, Spivey の Z のリファレンスマ ニュアルの第2版に準拠するものです. ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz から詳しい情報とオーダーフォーム を手に入れることができます.より詳しいことは Mike Spivey <mike@comlab.ox.ac.uk> と連絡を取ってください.
CADiZ は Z の仕様のチェックやタイプセッティングのためのツール 集です. 理解できる Z の方言は標準のものに置き換えます. タイプセ ッティングは, UNIX では troff と LaTeX が Windows では Word が利用可能 です. マウスを使って仕様を対話的に調べたり, 見たりすることができ, タイ プチェッカによって演繹された性質を調べたり,スキーマ計算式の展開を見た り, プルーフオブリゲーションのような推論式について推論を行なうことがで きます. PC 版は OLE2 をつかって MS Word と組み合わされていてZ のパラグ ラフを Word の文書の中で直接編集できる WYSIWYG を提供していま す. (troff と LaTeX の版は, 通常 ASCII のマークアップでテキストエディ タで編集します.) これらのツールは更に開発が進められています. CADiZ は BCS 賞を得た商品で Sun, SGI, PC 上で動作します. York Software Engineering, The Innovation Centre, York Science Park, Heslington, York, YO1 5DG, UK (email <yse@minster.york.ac.uk> , tel +44-1904-435206, fax +44-1904-435135).
ProofPower は 高階論理 (HOL) や Z での仕様記述や証明の支援を行なってく れるツール集です. ProofPower-Z の短期コースが要求があれば受けられま す. <ProofPower-server@win.icl.co.uk> にメールを送れば ProofPower に関 する情報が自動的に送られて来ます. さらに詳しいことを知りたければ, R.B. Jones, International Computers Ltd, Eskdale Road, Winnersh, Wokingham, BERKS RG11 5TT, UK (tel +44-118-969-3131 ext 6536, fax +44-118-969-7636, email <rbj@win.icl.co.uk> ) と連絡を取って下さい.
Zola は Sun workstation で動作する商業的な総合支援ツールで,仕様作成, 証明, 保守の全ての場面において自動的な支援をしてくれます. これは, シ ステム開発者のためのもので大規模な仕様を作成保守するために適した WYSIWYG のエディタ,タイプチェッカ, tactical theorem prover を備えてい ます. 詳細については, Chris Paine か Will Harwood, Imperial Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel +44-1223-462400, fax +44-1223-462500, email <fms@ist.co.uk> ) に問い合 わせてください.
ZTC これは教育目的の場合と非営利利用の場合のみ無料で利用可能なZ の型 チェッカです. これは Spivery の Z Reference Manual の第2版に準拠してい ます. zed や oz の LaTeX のスタイルと Z の ASCII 版の ZSL を受け付ける ようになっています. ZANS は Zのアニメータです. これはまた非常に粗野な 作りで, 研究段階の試作品です. ZTC と ZANS の両方とも Linux, SunOS 4.x, Solaris 2.x, HP-UX 9.0, Dos と extended DOS で動作します. これらは ftp://ise.cs.depaul.edu/pub/ の ZANS-x.xx と ZTC-x.xx でx.xx にはバージ ョン番号が入ります. 詳細については Xiaoping Jia <jia@cs.depaul.edu> と 連絡を取ってください.
Formaliser は文法指向の Z のエディタで型チェックを行なうことができて Microsoft Windows で動きます。これは Logiza Cambridge から入手可能です。詳 しいことは、Susan Stepney, Logica Cambridge Limited, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK (tel +44-1223-66343, email <stpneys@logcam.co.uk>) と連絡を取ってください。 あるいは http://public.logica.com/~formaliser/formlsr/formlsr.htm をみてください.
DST-fuzz は Mike Spivey による fuzz のパッケージをもとにしたツールセットで， Motif ベースのユーザインターフェイスで LaTeX のプリティプリント, 文法と型のチ ェックを行います． CASE ツールインターフェイスによってZのアプリケーションと構 造化仕様とをつなげることができます．これらのツールは SoftBench で開発されてい ます．詳しいことはHans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-(0)431-7109-478, fax +49-(0)431-7109-503, email <hmh@informatik.uni-kiel.d400.de>) と連絡をとってください．
B-Tool は Z による仕様の部分部分の関係の証明にチェックに使われます。これ は、Edinburgh Portable Compilers Ltd, 17 Alva Street, Edinburgh EH2 4PH, UK (tel +44-131-225-6262, fax +44-131-225-6644) によってライセンスされていま す。 更に詳しく知りたいかたは、 <support@epc.ed.ac.uk> の配布責任者に 連絡を取って下さい。
B-Toolkit は形式的開発法 B-Method を全てサポートするツールの集まりです。 B-Core (UK) Limited, Magdalen Centre, The Oxfor Science Park, Oxford OX4 4GA, UK. から入手可能です。更に詳細について知りたい人は、 Ib Sorensen (tel +44-1865-784520, fax +44-1865-784518, email <Ib.Sorensen@comlab.ox.ac.uk>) と連絡を取ってください。 または http://www-scm.tees.ac.uk/bresource/docs/B/btoolkit.html をみてください.
MS Windows と Machintosh のための Z のフォントが利用可能です. これら と Z のツールのリソースへのハイパーリンクに関しては, http://www.comlab.ox.ac.uk/archive/z.html#tools のページを参照してください.
Z のツールに関するサーベイは Colin Parker,Systems Process Department, W376C, British Aerospace, Warton Aerodrome, Warton, Preston PR4 1AX, UK によって作成 されたものがあります。
Next: どうやって Z について学べばよいですか?