Z その１

今日は、形式仕様のZ
Z/Eves（ぜっといーぶす）証明器を使ってやる話です。
Zは、公理的集合論に基づいている。

---

■基本的な書き方

スキーマを組み合わせて、システムができる。
→スキーマが記述単位＝仕様記述の単位

仕様記述の単位
　公理
　状態スキーマ
　操作スキーマ

---

■具体的な、スキーマの書き方

スキーマ名-------------------------------
| 状態変数：型
||変数？型　　　　　　　　　　　？は入力を示す
----------------------------------
|　事後状態’＝　事前状態＋・・・・　　状態の操作
----------------------------------

みたいな感じで書く。
ちなみに、　変数！　で出力

例

Hello-----------
|a:Z　　　　　　　　　Zは整数
|b:N　　　　　　　　　Nは自然数
-----------------
｜a' = a+b aにbをたしたものを、a'とする
-----------------

---

■Δ

スキーマをもってきて、りようすることができる。
上のHelloを使いたい場合

world------------------
|ΔHello;c:N
-----------------------
｜c'=a'+b+c
-----------------------

ΔHelloとやると、Helloで定義した、a,b,やa',b'が使える

---

■Ξ（ぐざい）

変化しないことを示す。
world------------------
|ΞHello;c:N
-----------------------
｜c'=a'+b+c
-----------------------
値を参照しかしないときなど・・・

---

■Z/EVES

メイン画面から、Editボタンをクリック。

NewParagraphを選ぶ→入力画面がでてくる

・「Box　Drawing」を使って、箱の線を描く

・箱の中の文字をキーボードから入力する

・入力したら、「File」ボタンをクリック、Doneをクリックすると、
　元のダイアログに入力される

・Commandのcheck all paragraphを選択すると、チェックしてくれる
　→左側に、YとかNとか出る。

・エラーがあるとき、そこをクリックして、右ボタン
　→Show　errorsでエラー表示

・メイン画面File→saveでセーブできる

---

とりあえず、ここまで