Z言語

Z言語（Z記法）について

Z言語（ゼットげんご）は、Z記法（ゼットきほう）とも呼ばれる形式仕様記述言語です。主にコンピュータシステムの記述やモデリングを行うために使用されます。この言語は、ZF集合論からその名を取り、次の2つの重要な側面に焦点を当てて設計されています。

1. コンピュータプログラムの簡潔な仕様記述：
Z言語は、プログラムの動作を明確かつ曖昧さなく記述するための手段を提供します。これにより、開発者は実装前にシステムの正確な振る舞いを定義できます。

2. 意図されたプログラムの振る舞いの形式的な証明：
Z言語を使用すると、プログラムの仕様が正しいことを数学的に証明するための形式的な枠組みを提供します。これにより、プログラムの信頼性が向上します。

歴史

Z言語は、1977年にJean-Raymond Abrialによって開発が開始されました。Steve Schumanとバートランド・メイヤーの協力のもと、初期の開発が進められました。その後、オックスフォード大学のプログラミング研究グループで開発が継続され、1980年代前半にはAbrial自身もこのグループで開発に携わりました。

Z言語の特徴

数学的基盤: Z言語は、公理的集合論、ラムダ計算、および一階述語論理といった、標準的な数学的記法に基づいています。
型付き: Z言語で記述されるすべての式は型付けされており、これにより素朴集合論に内在するパラドックスの一部を回避できます。
数学的ツールキット: Z言語には標準化されたカタログ（数学的ツールキット）が含まれています。このツールキットは、一般的に使用される数学的な関数や述語で構成されています。
記号の表現: Z言語は非ASCIIシンボルを多く使用しますが、仕様ではこれらのシンボルをASCIIやLaTeXで表現する方法も提案されています。

学習資料

Z言語を初めて学ぶ上で参考になる資料として、以下のようなものが挙げられます。

The Z Notation: a reference manual (英語)

実用例

Z言語は、IBMのCICSプロジェクトなどで実際に使用された実績があります。

標準化

国際標準化機構（ISO）は、2002年にZ言語の標準化作業を完了しました。この標準仕様は、"Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics ISO/IEC 13568:2002"という名称で、ISOから直接入手して閲覧できます。

ISO/IEC 13568:2002 : 13568_2002.zip（1MBのPDFファイル、196ページ）

関連技術

Z言語に関連する技術として、以下のようなものが挙げられます。

Z++
Object-Z
Z User Group (ZUG)
Community Z Tools (CZT) プロジェクト
形式手法
VDM
B-Method

参考文献・外部リンク

The Z Notation: a reference manual
Jonathan Bowen's The Z notation
Specification proposals by Ian Toyn
ISO公式仕様の購入 (Z言語)
Community Z Tools (CZT) プロジェクト
ZETA Zによるソフトウェア仕様記述のためのオープンソースシステム
Mike Spivey's Fuzz Type-Checker for Z
* Using Z: Specification, Refinement, and Proof (PDF文書を含む)

この記事は、2008年11月1日以前にFree On-line Dictionary of Computingから取得した項目の資料を元に、GFDL バージョン1.3以降の「RELICENSING」（再ライセンス）条件に基づいて組み込まれています。

もう一度検索