Z表記法を使用した形式仕様の例（スペイン語）。宣言と述語を含む名前付きスキーマボックス付き。

Z記法 （/ ˈ z ɛ d /）は、コンピュータシステムの記述とモデル化に使用される形式 仕様言語です。 [1]これは、コンピュータプログラムやコンピュータベースのシステム全般 の明確な仕様を規定することを目的としています。

歴史

1974年、ジャン＝レイモンド・アブリアルは『データセマンティクス』を出版した。[2]彼は後にグルノーブル大学で1980年代末まで教えられることになる記法を用いた。EDF（フランス電力公社）在籍中、アブリアルはベルトラン・マイヤーと共にZ記法の開発にも携わった。 [3] Z記法は1980年の著書『プログラミング方法』で使用されている。[4]

Zはもともと1977年にスティーブ・シューマンとベルトラン・マイヤーの協力を得てアブリアルによって提案されました。[5]その後、アブリアルは1979年9月にオックスフォード大学に着任し、1980年代初頭に 同大学のプログラミング研究グループでさらに開発が進められました。

アブリアルはZが「究極の言語だから」そのように名付けられたと述べている[6]が、Z表記法の「ツェルメロ」という名前もツェルメロ-フランケル集合論の使用を通じてZ表記法に関連付けられている。

1992年にZユーザーグループ（ZUG）が設立され、Z表記法に関する活動、特に会議やカンファレンスを監督するようになりました。[7]

使用法と表記

Zは公理的集合論、ラムダ計算、一階述語論理で用いられる標準的な数学表記法に基づいている。[8] Z表記法のすべての式は型付けされているため、素朴集合論のパラドックスの一部を回避できる。Zには、Z自体を使って定義された、一般的に用いられる数学関数と述語の標準化されたカタログ（数学ツールキットと呼ばれる）が含まれている。これはZスキーマボックスで拡張されており、 Zスキーマボックスは、標準の論理演算子に基づいて独自の演算子を使用することも、他のスキーマ内にスキーマを含めることによって組み合わせることもできる。これにより、Z仕様を簡単な方法で大規模な仕様に構築することができる。

Z表記法では多くの非ASCII記号が使用されるため、仕様にはZ表記法の記号をASCIIおよびLaTeXでレンダリングするための提案が含まれています。また、すべての標準的なZ記号にはUnicodeエンコードが用意されています。[9]

標準

ISOは2002年にZ標準化作業を完了した。この規格[10]と技術的正誤表[11]はISOから無料で入手できる。

  • この規格はISO ITTFサイトから無料で公開されており[10] 、別途ISOサイトから購入することもできる[10] 。
  • 技術的な正誤表はISOサイトから無料で入手できる[11] 。

賞

1992年、オックスフォード大学コンピューティング研究所とIBMは、「Z表記法の開発とIBM顧客情報管理システム（ CICS）製品への応用」により、技術的功績に対して共同で女王賞を受賞しました。 [12]

さらに読む

  • Spivey, John Michael (1992). Z記法：リファレンスマニュアル. 国際コンピュータサイエンスシリーズ（第2版）. Prentice Hall .
  • デイヴィス、ジム、ウッドコック、ジム(1996). 『Zを使う：仕様、詳細化、証明』 国際コンピュータサイエンスシリーズ. プレンティス・ホール. ISBN 0-13-948472-8. 2007年4月5日時点のオリジナルよりアーカイブ。2006年3月22日閲覧。
  • ボウエン、ジョナサン（1996）『Zを用いた形式仕様と文書化：ケーススタディアプローチ』International Thomson Computer Press、International Thomson Publishing . ISBN 1-85032-230-9。
  • ジャッキー、ジョナサン（1997年）『Zの道：形式手法による実践プログラミング』ケンブリッジ大学出版局、ISBN 0-521-55976-6。
  • インス, DC (1993).離散数学、形式システム仕様、Z入門.オックスフォード大学出版局. doi :10.1093/oso/9780198538370.001.0001. ISBN 978-0198538370。

参照

参考文献

  1. ^ Bowen, Jonathan P. (2016). 「Z記法：原因はどこから、そして進路はどこへ向かうのか？」(PDF) .信頼できるソフトウェアシステムのエンジニアリング.コンピュータサイエンス講義ノート. 第9506巻. Springer . pp.  103– 151. doi :10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2。
  2. ^ Abrial, Jean-Raymond (1974)、「データセマンティクス」、Klimbie, JW; Koffeman, KL (編)、Proceedings of the IFIP Working Conference on Data Base Management、North-Holland、pp.  1– 59
  3. ^ Hoare, Tony (2011). 「ベルトラン60歳の誕生日に寄せて」(PDF) . ナンツ, セバスチャン (編).ソフトウェアエンジニアリングの未来. Springer . pp.  183– 184. doi :10.1007/978-3-642-15187-3. ISBN 978-3-642-15187-3。
  4. ^ ベルトラン・マイヤー; Baudoin、Claude (1980)、プログラムの方法(フランス語)、Eyrolles
  5. ^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980)、「仕様言語」、Macnaghten, AM; McKeag, RM (eds.), On the Construction of Programs、Cambridge University Press、ISBN 0-521-23090-X(言語の初期バージョンについて説明します)。
  6. ^ Hoogeboom、Hendrik Jan. 「ソフトウェア エンジニアリングにおける形式的手法」(PDF)。オランダ:ライデン大学。2017 年4 月 14 日に取得。
  7. ^ Bowen, Jonathan (2022年7月). 「Zユーザーグループ：30年後」(PDF) . FACS FACTS . No.  2022–2 . BCS-FACS . pp.  50– 56. 2022年8月3日閲覧。
  8. ^ Spivey, J. Michael (1992). 『Z記法：リファレンスマニュアル』 国際コンピュータサイエンスシリーズ（第2版） ヘメル・ヘムステッド：プレンティス・ホール. ISBN 978-0139785290。
  9. ^ Korpela, Jukka K. 「Unicodeの説明：文書、プログラム、Webサイトの国際化」。unicode -search.net。2020年3月24日時点のオリジナルよりアーカイブ。2020年3月24日閲覧。
  10. ^ abc "ISO/IEC 13568:2002". 情報技術 — Z 形式仕様記法 — 構文、型システム、セマンティクス( Zipped PDF ) . ISO. 2002年7月1日. 196ページ。
  11. ^ ab "ISO/IEC 13568:2002/Cor.1:2007". 情報技術 — Z 形式仕様記法 — 構文、型システム、セマンティクス — 技術訂正票1 (PDF) . ISO. 2007年7月15日. 12ページ
  12. ^ 「1992年女王技術功績賞」オックスフォード大学コンピューティング研究所。2008年12月2日時点のオリジナルよりアーカイブ。 2021年10月17日閲覧。