演習3第3期

今日が、とりあえず最終日。なんで、演習3はこれで全部終わり。なんか、中間発表の時より準備不足で中身も薄くて、ぐでんぐでん。
第3期はSPINというモデルチェックツールを使うというテーマで、うーん。誰かが言ってた型推論C++の方がおもしろかったかもしれぬ。それはそれで、いろいろと技術的な問題や、topicがありそうだし。
最後までぬぐいきれなかったある種の違和感が、さっき寝たらちょっと分かった気がする。これって、状態遷移でモデル化されたプログラムが、ある種の性質を満たすか満たさないかを検証してくれるというツールであるわけだが、このモデル化の作業に何か違和感を感じてならなかった。つまりプログラムのソースを渡されて、「これが正しいかチェックしてよ」という類のツールでは無い。ソースからモデルを作るというのは、つまりソースから仕様書を起こすという、例のダメプロジェクトのパターンで、その作業を慎重に行えないと正しくモデル化できないし、慎重に行ったら問題も自然に発覚する気がする。だから、本当の使い方としては、プロジェクトの初期に対象の問題をモデル化、この時点でモデル検証を行い、その仕様で問題ないことを確認してからプログラムを書くって形になるんではなかろうかと。
じゃぁ世の中そんなにうまく回っているかというと、プログラム課題をやるたびに「よーし、仕様書書いちゃうぞ」なんていう人いないわな。だいたい仕様なんて、次の日会社に行くと変わるもんで、その都度global変数（含member変数）をアドホックに増やして、さくさく怪しくなっていくわけですよねぇ。で、そうするとプロジェクトチームの体質の問題ってことになって、ってぇとぉ、なんだ？　そうそう。世の中、global変数は危ないからmember変数にしろってことになってるけど、オブジェクトが巨大化したら大差ないと思うんだけど・・・。まぁ、巨大化しないように区切りなさいってことですが。
でも、あれだよね。モデル化＝仕様書を書くための言語があるんだったら、そこから自動的にプログラムを生成してくれればいいのに。それはなんか違う？　うーん。