スクリプト言語へのモデル検査のサンプルプログラムを書いてみた

「モデル検査のゲームシナリオへの適用」にて、モデル検査を実開発に適用するのための基本の基本の部分を説明し終わりましたので、実際に、説明用の超簡易スクリプト言語へ、説明したモデル検査手法を適用してみるサンプルプログラムを作ってみました。

まずは、シンプルに Java のコンソールアプリとしてサンプルを作りました。が、それだけではイメージがわきにくい気がしましたので、この機会にと、以前から少しずつ触っていた Eclipse Plugin でも実装してみました。実装してみたといっても、検証を1ステップごとに実行できるだけで、たいしたものではないのですけれど。

これらのモデル検査のサンプルプログラムは、検査対象が実用にはほど遠いオモチャの言語ですので、即実用というわけではありません。しかし、各自のスクリプト言語へパーサやモデル検査器をカスタマイズしていけば、それなりに短い工数で評価してみることくらいはできるのではないかと思います。

しかし、想像以上に、というか想像通りというか、日曜 Java プログラマにはなかなかハードでした……orz。そもそも、オブジェクト指向でまともな規模のプログラムを書いたのも久しぶりという体たらくでしたので、いいリハビリになります（＾＾；だいぶん、コードの手本（コピペ元ともいう）を探してくる術が身につきつつありますので、少しは楽になるといいんですが……。

ただ、実装していて、そもそもオブジェクトの生存期間とか、どのスレッドがどれに触っているのかとか、動けばいいや！でほとんど考えてないので、規模が大きくなった頃にレースコンディションで泣いたりしそうな気がひしひしとします。でも、そのときはそのときのことです。製品になるコードじゃないんですし！