形式手法とHaskellについてメモ

いけがみさんの記事を読みながら、思ったことをメモ。
＃まとまっていないので、あくまでも妄想です。

【元ネタ】
Inemuri nezumi diary(2009-02-05)

2009-06-23 - a-sanの日記
不正な状態遷移を見つけるアルゴリズム - a-sanの日記

僕が形式手法に興味を持った理由は、設計工程でモデリング作業の品質を上げることができて、更にテストケースを生成してくれるのではないか、という期待があったから。
でも、形式手法は確かに凄いのかもしれないが、言語もツールもオープンでないので使いづらい。
いけがみさんの言う通り、完璧な仕様を求めようとして、結局無駄な力を注いでいるのかもしれない。

モデリングは結局、事前条件と事後条件をつなげて一貫性と整合性が取れているか、そして状態遷移図が矛盾なく整合性が取れているか、という作業に落ち着くと思う。
関数型言語Haskellでも、形式手法でやりたかったことが同様にできるのではないか？

少なくとも、「不正な状態遷移を見つけるアルゴリズム - a-sanの日記」にあるHaskellのプログラムは、状態遷移図の整合性チェックができることを示しているように思う。

Haskellも僕にとって難しかった。
モナドや遅延評価だけでなく、関数型言語そのものの発想がないから。

でも、プログラムだからいくらでも試せる。
Howを考えるのではなく、Whatを考えるようにHaskellプログラムを書けばいい。
Haskellを書きながら、問題設定を考えながら、仕様を考えているのだ。
できれば、Haskellプログラムからテストケースを生成したい。

現在、考えている荒筋は下記の通りだ。

MSのPairwise法ツールPICTをエンジンに持つテストケース自動生成ツールMTGに状態遷移表を書けば、パラメータの組み合わせを生成してくれる。
その結果をTestLinkCnvMacroに貼り付けて、ちょっとだけフォーマットを整えれば、テストケースを出力できる。
そのテストケースをTestLinkへインポートすれば、TestLink上でテスト作業を一括管理できる。

つまり、質の良いテストケースを出力できれば、後はTestLinkでテスト作業をコントロールすればいい。
そのために、MTG→TestLinkCnvMacroのツールを使う。

MTG プロジェクト トップページ - SourceForge.JP

TestLinkCnvMacro - SourceForge.JP

後は、MTGへ吐き出すためのパラメータや制約条件がHaskellや形式手法、あるいはUMLの状態遷移図から作れればいい。
実際は、その部分が自動化できておらず、手作業になっている。

チケット駆動開発や構成管理に比べると、テスト工程の自動化はとても難しいが、どこまで可能か考えてみたい。