すごく分かりやすい資料があった
「フォーマルメソッド導入ガイダンス」をざっと読み流すつもりでしたが、それでもなかなかのボリューム感がありました。そろそろプログラム触ってみたいと思っていたところ、導入としてすごく分かりやすい資料を発見。作成日も新しい。知りたかったことが、ずばりとまとめられている。嬉しい。とっかかりの人は、この資料から入ると分かりやすいと思います。
ほかにも良い資料・サイトをご存知の方がいらっしゃれば、教えていただければ幸いです。
やはり使いどころが難しい
感想としては、形式手法を適用するコストはやはり高く、システム全体に適用するのは現実的ではなさそう。
効果的な箇所に絞って適用するのが良いと思いました。方向性としては、以下のような箇所でしょうか？
- 制御・状態遷移が複雑で、多様な使われ方をするプログラム → 品質確保が難しそう
- 品質リスクの大きいプログラム → 品質確保のコスパが高そう
- 他のシステム・プログラムから共通して使用されるプログラム → 使用頻度が高く、品質確保のコスパが高そう
- 他のプログラムとの境界が明確 → 定義しなければならないルールの範囲が明確
具体的にいえば、以下のような箇所が良いという印象です。
- フレームワーク
- 共通部品
- API
確かに、対象ドメインの知識が必要そう。ハードルが高い
上記の資料のなかに、形式手法を認証制御に適用検証した事例がありました。
まさにこういう箇所が、適しているという感想です。
認証制御は私も実装したことがありますが、制御が結構複雑です。全体の制御をきちんと理解して、神経をはりめぐらせていないと、いろんな落とし穴にはまってしまいます。
例えば、管理者が一人しかいない状況で、その管理者がパスワードを忘れるとシステム全体として詰んでしまいます（パスワードを再設定できるのは管理者だけだが、その管理者がいない）。
こういった仕様バグを抽出するには、制御の全体が分かる人が頭の中で「困ったことが起こらないか」を考えていくしかありませんでした。うまくバグを抽出できるかはその人次第になります。チェックリスト等を作ったところで抽出することはできません。形式手法が適していそうです。
これを形式手法で定義していくためには、まず「利用者がパスワードを忘れる」という状態を思いつく必要があります。システムの外側（人間側）にある状態なので、認証制御の開発・運用の経験がないと考慮がもれてしまいそうです。
「形式手法の適用には対象ドメインの知識が必要」というのは、こういうことなのかと腹に落ちました。ハードルが高い……。
いや、そろそろプログラムに触りたくね？
と、感想ばっかり書いても仕方ないので、プログラムにもう触ります。
でも仮説をもって技術に触れるのは、検証の観点も明確になっていいことだと思う……という言い訳。
自分の妄想がどこまであっていたか、プログラムに触りながら答え合わせをしていきたいと思います。