Z その３ 証明とテスト

わすれそうなので、ちょっとメモ

---

■証明方法

theorem なんとか
　条件

という形で、証明したいことを書く。

まず、編集して、command→check all paragraphを行うと、
proof（左から２番目）がNになるときがある

このとき、証明できていないので、自分で証明する必要がある。
Nのところを選択して、右クリックすると、

　　　Show　Proof

というのがでてくる。それを選択すると、新しいダイアログが開く。
下に、式が書いてある。

　　全部選択して、
　　Reductionボタンをクリック、
　　prove by reduceをやってみる

うまくできたら、それでよし

うまくいかなかったら、自分で証明する必要があるので、適当に選んで
　　Reductionボタンをクリック、
あぷらいなんとかとか、simplifyとかあるので、てきとーに選ぶ

---

■theorem以外で、ProofがNになる。

　theoremをかかなくても、条件上、証明しないといけないときに起こる。
　この証明は、windowボタンのtheoremsを見ればわかる。
　そこから見たいものをダブルクリック。右側に証明がでる。

　ちなみに、これを直したいなら、specification画面に戻って、
普通の証明のように、右クリック、show proofを出す。
　あとは、証明できる。

---

■テスト

　この証明を使って、テストすることができる。
　スキーマ名[変数名 := 値]
　の形で書くと、値が設定できる。

　そこで、こうなっていてほしいという（要するに事後条件）を
　theoremで書けば、証明のチェック（演繹）で、値の変化や、正しいかどうかがわかる。

RFPの目標とかを受けて、提案書になって、その提案書が要求仕様書にはいるよねえ？

　あれ、ちょっと気になったので・・・
　RFPと提案書と要求仕様書の関係。

　RFPで、ふつう、
　　・提案してもらいたいシステムの概要（範囲とか、背景とか）
　　・目的・目標ないしはゴール（課題の場合もある）
　を書くよねえ（ここもそうだし、ITコーディネーター協会のRFP/SLA見本もそう）

　で、その目標や目的、課題などを受けて、提案書が作られる。

　さすがに要求仕様書は、提案書とは無関係に書けず、
　目的・目標、課題にかんするソリューションは、
　要求仕様書にはいってきて、

　その際、IEEE830だと、１章の「はじめに」の目的、範囲が、RFPの目的やその他もろもろに合致しているはずってことになるんだよねえ・・・

　対応関係で言うと・・・

VDMのお勉強－その７ VDMを書こう！ VDM++版概略

シリーズ「VDMのお勉強」。

前回は、VDM－SLで、「名前を入力したら、
　”Hello ”＋名前＋”!!"
と出力する処理、Helloを定義」した。
今回は、ついでに、まったく同じコトを、VDM++で定義してみたいと思う。

---

■overtureの出力

　overtureで、VDM++のクラスを生成すると、自動的に以下のように書かれる。

class HelloVDM
	types
-- TODO Define types here
	values
-- TODO Define values here
	instance variables
-- TODO Define instance variables here
	operations
-- TODO Define operations here
	functions
-- TODO Define functiones here
	traces
-- TODO Define Combinatorial Test Traces here
end HelloVDM

---

■サンプルコード

これに、上記のメソッドを書くんだけど、昨日のVDM-SLと同じように直す。
そうすると、こんなかんじ

class HelloVDM
types
--	ここに、型とか書くけど、今回は使わない

values
--	ここに、定数とか書くけど、今回は使わない

instance variables
--	ここに、インスタンス変数とか書く
-- public(private) 変数名 : 型 := 初期値; の形で書くけど、今回は使わない

-- 	不変条件
--     inv 条件式の形で書くけど、今回は使わない

functions
-- 関数を書くんだけど、今回は使わない

operations
public Hello : seq of char ==> seq of char
Hello(名前) ==
(
	return "Hello " ^ 名前 ^ "!!"
)

-- 事前条件：
pre len 名前 > 0;

-- 事後条件：
-- post 条件式だが、今回は特にない

traces
-- これを使って、あーしてこーしてテストすると、
-- かっこよく出来るんだけど、そもそも、今回テストしない

end HelloVDM

---

■そして

　このソースを、VDM++用のVDM toolで開く。
VDM++用なんだけど、使い方は、
VDMのお勉強－その４　使い方
http://blog.goo.ne.jp/xmldtp/e/e08a21fa14c65253fa145563935571bb
で書いたVDM-SL用ツールと同じ。

まず、プロジェクト→ファイルの追加で読み込み、
　　　車両通行止めみたいなアイコンをクリックすると、実行ウィンドウが出てくる。

そこで、

init
create h := new HelloVDM()
debug h.Hello("vdm")

と入力すると、上の実行ウィンドウに

"Hello vdm!!"

と表示される。

12月1日(水)のつぶやき

09:38 from web
国交省のアンケート、大都市交通センサスかいてるんだけど、利用路線、「地下鉄」の書き方が判らない！JRは、東日本旅客鉄道と書くらしいけど、そうすると、地下鉄は（営団でなく）東京地下鉄？でも、東京地下鉄丸ノ内線だと、欄に入らない…
09:44 from web
まじ！iPadでastah*が動くの？ RT @hiranabe : astah* の iPad版、ET2010にて展示（ET2010 東洋テクニカさんのブース）。全くの新規開発で、手軽にほいほいクラス図描けます。触ってみてください。
by xmldtp on Twitter