VDM++

VDM++ は、オブジェクト指向仕様記述言語であると同時に、 関数型言語 の機能を持った仕様記述言語でもあるので、モデルを作る際 「オブジェクト指 向」であることにこだわることはない。 一般に、関数型指向でモデルを作成し た方が抽象度が高く、 行数も少なくモデルを作成できることが多い。 オブジェ クト指向モデルは、より詳細な、 設計よりのモデル化に向いている。

1. 要求を読む・聞く

2. 主に名詞からデータ型とクラスを、 主に動詞から関数または操作を抽出 する

3. 型とクラスと関数・操作のシグネチャの概略を書く

4. 要求から不変の性質を見つけ、型やインスタンス変数の不変条件を記述 する

5. 関数・操作の事後条件、事前条件を記述する

6. 関数・操作定義を完成させる

7. できるだけ段階的洗練を使う

8. 仕様に矛盾がないか検証する

9. 構文チェック、型チェック、 テスト、 証明課題生成、 証明によって検証 と妥当性検査を行う

10. 要求をレビューし、 漏れがないか再検討する

雑な書き方

集合束縛

code:_

p1, p2, ..., pn in set 式e

関連