Z言語

ウィキペディア

索引トップ用語の索引ランキングカテゴリー

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/09/23 07:30 UTC 版)

ナビゲーションに移動検索に移動

コンピュータプログラムの簡明な仕様の記述。
意図するプログラムの振る舞いの証明の形式化。

Zは、もともとは1977年に Jean-Raymond Abrial により Steve Schuman とバートランド・メイヤーの支援を得て開発された^[1]。 Zの開発は、オクスフォード大学のプログラミング研究グループでさらに続けられた。 Abrial は、1980年前半にこの研究グループで開発作業を行った。

Zは、公理的集合論とラムダ計算、一階述語論理で使われる標準的な数学的記法に基づいている。 Zで記述されたあらゆる式は型づけられており、それにより素朴集合論のパラドックスのいくつかを回避する。 Zは標準化されたカタログを含む。このカタログは数学的ツールキットと呼ばれる。このツールキットは、一般的に使われる数学的な関数と述語から構成される。

Zは多くの非ASCIIシンボルを使っているが、Zの仕様ではZで使うシンボルを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から直接に取得し閲覧することができる。

13568_2002.zip、1 MB PDF、196 頁

外部リンク

この記事は2008年11月1日までGFDLバージョン1.3以降の再ライセンス規約に基づいていたFree On-line Dictionary of Computingにある項目の資料が元になっている。

参考文献

^ Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer A Specification Language, in On the Construction of Programs, Cambridge University Press, eds. R. McNaughten and R.C. McKeag, 1980 (Zの初期のバージョンを記述)

[前の解説]

「Z言語」の続きの解説一覧