Loading article…
Z表記法/ ˈzɛd /は、コンピュータシステムを記述およびモデル化するために使用される形式仕様言語です。[ 1 ]これは、コンピュータプログラムおよびコンピュータベースのシステム全般の明確な仕様を目的としています。
1974年、ジャン＝レイモン・アブリアル[ 2 ]は「データ意味論」[ 3 ]を出版した。彼は後に1980年代末までグルノーブル大学で教えられることになる記法を用いた。
EDF（フランス電力公社）に勤務していた頃、ベルトラン・メイヤーと共に、アブリアルはZの開発にも取り組んでいた。[ 4 ] Zはもともと、1977年にスティーブ・シューマンとベルトラン・メイヤーの協力を得てアブリアルによって提案された。[ 5 ] Z記法は、1980年の書籍『プログラミングの方法』で使用されている。[ 6 ]
Z は、オックスフォード大学のプログラミング研究グループでさらに開発されました。アブリアルは、1979 年 9 月にオックスフォードに到着し、1980 年代初頭にバーナード・スフリンやイブ・ホルム・ソーレンセン(1949–2012) [ 7 ]などの研究者とともに同グループで研究を行いました。 [ 8 ]ソーレンセンは、初期の Z ベースの研究で 1981 年にオックスフォード大学から博士号を取得しました。 [ 9 ]彼はオックスフォードで Z 記法の初期のコースを教え[ 10 ]、最初はオックスフォードで Z ユーザーミーティング シリーズを設立しました。[ 11 ]
イブ・ホルム・ソーレンセンは、 IBMハーズリーと共同で、1982年の発足当初からオックスフォード大学のトランザクション処理プロジェクト（後に「CICSプロジェクト」と改名された[ 12 ] ）を率いた[ 13 ]。このプロジェクトでは、Z記法を用いてIBMのCICSトランザクション処理ソフトウェアの一部を正式に規定した。これは1992年にクイーンズ・アワード・フォー・テクニカル・アチーブメントを受賞した[ 14 ] [ 15 ]。CICSプロジェクトの一環として、ソーレンセンは、抽象コマンドとしてZスキーマ記法の使用を可能にすることで、エドガー・ダイクストラのガード付きコマンド言語を拡張した[ 16 ] 。これらのアイデアは後にキャロル・モーガンによって、彼の改良計算で形式化された[ 16 ]。
Zスキーマボックスは、より大規模な仕様の構造化のためにキャロル・モーガンによって追加されました。 [ 17 ]イアン・ヘイズは、モーガン、ソーレンセン、スフリンらの寄稿を含む、Zの使用に関する1987年の書籍「Specification Case Study」 （第2版は1993年出版）を編集しました。 [ 18 ] Zの事実上の標準は、1989年にマイク・スピビーによって書籍として作成されました（第2版は1992年）。[ 19 ]
アブリアルは、Z が「究極の言語だから」という理由でそのように名付けられたと述べている[ 20 ]。ただし、「ツェルメロ」という名前は、ツェルメロ・フレンケル集合論の使用を通して Z 記法とも関連付けられている。
Z は、公理的集合論、ラムダ計算、および一階述語論理で使用される標準的な数学的記法に基づいています。[ 19 ] Z 記法のすべての式は型付けされているため、素朴集合論のパラドックスの一部を回避できます。Z には、Z 自体を使用して定義された、一般的に使用される数学関数と述語の標準化されたカタログ (数学ツールキットと呼ばれます) が含まれています。Zは、標準的な論理演算子に基づく独自の演算子を使用して組み合わせることができ、またスキーマを他のスキーマ内に含められるZ スキーマボックスによって拡張されます。 [ 17 ]これにより、Z 仕様を便利な方法で大規模な仕様に構築できます。
1985年、イブ・ソーレンセンによって一連のZユーザーミーティングが、最初はオックスフォードのルーリーハウスで開始されました。[ 11 ] 1992年、これらのミーティングの1つで、Z記法に関する活動、特にミーティングや会議を監督するためにZユーザーグループ（ZUG）が設立されました。 [ 11 ] ZUGは、定期的なZユーザーワークショップ/ミーティング（ZUM）を組織し続けました。その後、英国以外で開催されるようになると、これらは国際Zユーザー会議として知られるようになりました。さらにその後、これらの会議はBメソッドも対象とするように統合され、国際BおよびZユーザー会議（ZB）として知られるようになりました。
ISOは2002年にZ規格の標準化作業を完了しました。この規格[ 21 ]と技術訂正[ 22 ]はISOから無料で入手できます。
Z表記法は非ASCII記号を多く使用するため、仕様にはASCIIとLaTeXでのZ表記記号のレンダリングに関する提案が含まれています。また、すべての標準Z記号にはUnicodeエンコーディングがあります。 [ 23 ]
1992年、オックスフォード大学コンピューティング研究所とIBMは、「Z表記法の開発とIBM顧客情報制御システム（ CICS ）製品への応用」により、共同で女王技術功績賞を受賞しました。[ 24 ]