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でセーブできる

---

とりあえず、ここまで

astah*を使って、ICONIX風一気通貫システム開発 その３：ユースケースシナリオ

　「astah*を使って、開発の要求仕様から、プログラム作成までを、トレーサビリティを保って、どのように開発するかを書いてみる」という、このシリーズ、以下の手順で説明する予定ですが、

（１）作るべきもののユースケースを書く
（２）ユースケースシナリオを書く
（３）ロバストネス分析
（４）バウンダリ（画面）、エンティティ（テーブル等）の属性を埋めていく
（５）バウンダリの項目を元に、画面構成を考える。
（６）(必要があれば）エンティティを正規化して、ER図にする
（７）フレームワークを決定する
（８）画面クラスをソースコードに書き直す
（９）エンティティをDBのテーブルと、DAOに書き直す
（１０）コントローラーを書き直す

前回、（１）をやったので、今回は、「（２）ユースケースシナリオを書く」について。

---

■ユースケースシナリオを書く

　ユースケース図を描いたら、各ユースケースに対して、処理概要とか、処理内容等、ユースケースシナリオと呼ばれるものを書きます。

　astah*の場合、（コミュニティ版ではなく、お金を払った）UML版、プロフェッショナル版などだと、ユースケースを右クリックして、ポップアップメニューを出すと、ユースケース記述（シナリオ）が書けるメニューがでてくるので、それを選ぶと、表示されます。

　なお、Enterprise Architectだと、シナリオとして、ユースケースシナリオが書けるけど、かわりに、アクティビティ図で書くこともある。

　ユースケースシナリオとして、書く内容は、

ユースケース記述
http://www.atmarkit.co.jp/aig/04biz/usecasedescription.html

　に書いてある。だいたい、こんなことを書く

・ユースケース名
・基本系列・代替系列
・事前条件・事後条件

以下、くわしくみていく。

---

■基本系列・代替系列

　基本系列は、正常系の処理を書くことになる
　代替系列は、正常系ではないものを書くんだけど、このとき、例外がある場合と、ない場合がある。ない場合は、例外も混ぜて書いていい。

　たとえば、

・ログインすると表示される
・アカウントがない場合は、アカウント作成
・ログイン名とパスワードが間違っていたら、エラー表示

の場合、基本系列と代替系列、例外とある場合は、

基本系列
　　・ログインすると表示される
代替系列
　　・アカウントがない場合は、アカウント作成
例外
　　・ログイン名とパスワードが間違っていたら、エラー表示

となり、例外がない場合は、
　
基本系列
　　・ログインすると表示される
代替系列
　　・アカウントがない場合は、アカウント作成
　　・ログイン名とパスワードが間違っていたら、エラー表示

または、
　
基本系列
　　・ログインすると表示される
　　・アカウントがない場合は、アカウント作成
代替系列
　　・ログイン名とパスワードが間違っていたら、エラー表示

ってなかんじなのかしら・・・
（どっちになるかは、書き手とか、会社の考えなのかしら？）

基本系列は、箇条書きで番号を振っていき、その番号に対応する形つまり、

　　基本形列番号－枝番

で、代替系列を書くと、あとの工程（ロバストネス分析）で楽になる

---

■事前条件・事後条件

　事前条件、事後条件は、検証で言う事前・事後条件と、ちと違う場合がある（同じ意味に使う人もいる）

　ユースケースシナリオなど、UML関係で言う場合は、

ユースケースを実行する前の状態

（上記斜体は、上記サイトより引用）

だが、検証をやっている人にとっては、事前条件とは、

不変条件を満たすため、その処理を行う前に、満たさなければならない「条件」だ。

ちなみに、不変条件とは、常に満たさなければならない性質ということになる。
ここで言う性質とは、値の範囲や、クラス間の関係などをさす。

---

■検証で言う事前条件と、UML関係でいう事前条件の違いの例

「象を冷蔵庫に入れる」というユースケースを考える。

●UML関係だと、冷蔵庫に入れる前の「状態」を書くのだから、事前条件は、

・象を捕まえておくこと

になる。

この場合、象さえ捕まえれば、冷蔵庫には、「入れられる」

●一方、検証の世界でいう事前条件を考える。

冷蔵庫には、入れられる容量というものがある。
これ以上入れようとしても、入れなれない。これは、常に成り立つので、不変条件。

・不変条件：
　　０＜＝冷蔵庫に入っているもの　＜＝　冷蔵庫の収納容量

象を冷蔵庫に入れる場合、不変条件を満たすために

入れようとしているものの容量
　　＋現在の冷蔵庫に入っているもの　＜＝　冷蔵庫の収納容量

とならなくては成らない。これが、事前条件。
したがって、冷蔵庫が冷凍倉庫のように、大きいものなら入るけど、
家庭用の冷蔵庫の場合、収納容量がそんなにないので、

この場合、象を捕まえても、冷蔵庫には、「入らない」
　　→事前条件違反

---

■事前条件・事後条件と、実装との関係

　したがって、検証における事前条件は、
　　　実装時、処理開始前に行う、エラーチェック項目

　となり、検証における事後条件は、
　　　実装時、JUnitなどのアサーションで確認すべき、テスト項目

　となる。


　一方、UML関係の事前条件は、
　　　処理の前後関係を示す程度である。

　事後条件は、
　　　テスト項目にしてもいいかもしれない。

　DbC（契約による設計）の場合は、どっちかというと、検証よりにしないとまずいか？
　ま、どっちよりに書くかは、会社や書き手、上司のセンスなどによって、異なる。
　ただ、検証よりのほうが、実装のとき、こまらないね。

---

こんなかんじかしらね・・・
次回は、ロバストネス分析

11月24日(水)のつぶやき

16:33 from web
あとでよむ：Amazonクラウドに対応したオープンソース動画配信プラットフォーム「Kaltura 3.0」リリース http://sourceforge.jp/magazine/10/11/22/0344242
by xmldtp on Twitter