私的メモ：仕様記述言語「Z」の読書メモ

next49 @next49

赤間 世紀： 仕様記述言語「Z」

next49 @next49

表紙の”「仕様」の数学的構造化に「自然言語」を使う！”って正しいのかな？Zはどう考えても人工言語だけど。

next49 @next49

p.7 一般に「毛意識的」という言葉は、「数学的」と同じ意味で用いられる

next49 @next49

「要求仕様」は要求をまとめたもの

next49 @next49

「設計仕様」はどのようにシステムを構成するかを明確にしたものをまとめたもの

next49 @next49

「実装仕様」はプログラムのこと

next49 @next49

「テスト仕様」はどのようにテストを行うのかをまとめたもの

next49 @next49

「テスト仕様」はどのようにテストを行うのかをまとめたもの

next49 @next49

「運用仕様」はどのようにシステムを稼働させることができるのかをまとめたもの。すなわち、ユーザーマニュアル

next49 @next49

「保守」は、実際の運用で発生する問題などに対応すること。「保守仕様」は、どのように保守を行うのかをまとめたもの。

next49 @next49

要求定義、設計が上流工程。実装、テスト、運用、保守が下流工程。

next49 @next49

p. 9 「実装」が「仕様」を満たしているかを確認する作業を「検証」という。

next49 @next49

「形式仕様」は仕様を形式化したもの「形式検証」は、実装が仕様どおりにできているかを検証するさいに形式手法を用いて数学的に検証すること。似たような表現だけど、前者はもの、後者は行為。

next49 @next49

Zは2002年にISOで標準化されている。Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics ISO/IEC 13568:2002

next49 @next49

Zを「ゼッド」と読む理由は、開発がオックスフォード大学なので、イギリス英語の発音に準拠しているため。Zの由来は、公理的集合論ZFのZから。

next49 @next49

Zは一階述語論理と公理的集合論を統合した言語。

next49 @next49

p. 12 Zの特徴。1) 厳密な理論基礎がある。 2) 数学的構造化ができる 3) 自然言語を用いる 4) システムの改良ができる

next49 @next49

p.61 からのZの説明がさっぱりわからない。説明なしの用語が出すぎだ！

next49 @next49

pp 59 - 127 「第3章 Z言語」の説明の仕方が私には合わない。基本要素から組み立てていくのではなく、私が理解できていない何らかの順番ですべての要素を説明していくので、何のことやら。ただし、使われている用語、概念は全部理解できる。

next49 @next49

一階述語論理の基礎、集合論の基礎まで分かっていればどうにか使えそう。

next49 @next49

スキーマ、公理的記述はどういう関係になっているんだ？スキーマの構成は一体どうなっているんだ？

next49 @next49

Zでかかれた仕様について自然演繹で証明できるのは、わかったけど、それとスキーマの関係は？

next49 @next49

p. 163 オブジェクト指向に対応して、Zを拡張したObject -Zがあるらしい。Object-Zには時相論理が取り組まれている。

next49 @next49

The Z Notation: a reference manual http://spivey.oriel.ox.ac.uk/mike/zrm/index.html

next49 @next49

Community Z Tools http://czt.sourceforge.net/