「形式手法ってなんだろう」について
はじめに
久しぶり、私のブログよ・・・ってほど放置してたわけですが、セッションの言い訳記事を書くっていっちゃったので今回のwacate2019冬セッション「形式手法ってなんだろう」について書きます。きっとクリスマスイブだからだれも気が付かない・・・はずだ！
書くとは言ったものの、Twitterでも書いた通り、今回技術的にも精神的にも本当に限界だったため、補足的なものはあまり書けないのです。
ですので、成り立ちという名の言い訳と、自分がセッションやってみての感想がメインになります 。ご了承ください。
セッションの成り立ちという名の言い訳
wacateに参加された皆さんはポジションペーパー集をみれば、なぜこんなセッションを私がやろうと思ったのかが書いてありますが、はしょって説明すると、難しいセッションを難しいセッションとして、やり切ってみたかったっていう話です。そのお題として「形式手法」を選んだのもいろいろ自分本位な理由があるんですが、まあいいです。
とにかく、取っ掛かりとしてはしょうもない理由で始めたセッションだったのですが、今回は、自分が形式手法を勉強しつくすという観点もさることながら、「形式手法」で「ワークをやる」にはどうすればたどり着くのか、ものすごく悩みました。
具体的に、トピックとして3点（結果的に）工夫？しました。
- モデリングの話はしない
きっと講義形式にしておけば、丁寧にモデリングの話をして、形式手法本体へ・・・ってできたと思うんです。というか、それが普通だと思います。しかし、今回は中心に「ワーク」をおいてしまっていたため、モデリングの話はほぼせず、「厳格に仕様を書ける、検証できる！」にしぼって説明しました（実際はとってもひよってて、wacate実行委員のレビューのたびに無駄に「モデリングの話はしない！」と宣言してた気がします。。）
せめて井芹さんのセッションへの導線は張ろうと思ってたのですが、当日ふっとびまして・・・orz。しかも、しっかり拾っていただいたようで、ほんとうにいろいろとごめんなさい。 - 形式手法の文法の話はほとんどしない
実は、今回のスライド群の中で一番初めにできたのは、補足にあるVDM++のページでした。あれ、みんな、参考文献のコピペだと思ってるでしょう？違うんです！VDM++って、資料は多くても、プログラミング言語みたいな逆引きリファレンスとか記述例をまとめたものは少ないんです。だから、少しでもわかりやすくしようと思って、例とか意味の表記とか、工夫して必死で書いたんです。当初は説明しようかとかワークのときに配ろうかとも思ってたのですが、ノイズになるっていうレビューでのきっちり再三（4回かもしれない）の指摘によりお蔵入りしました。。。
実際のセッションでは、使用する文法をしぼり、すべてワークシートに文法から意味から記載することによって、少しでもワークで「形式手法に触れる、実感する」ということがしやすいように工夫しました。 - 検証の話をきもち、強めにした
最初できたスライド案では、検証の話はもうちょっとページが少なかったのです。というのも、「ワークどうしよう」という気持ちの焦りから、検証の部分がどうしても後回しになっていました。
そんなとき、とある実行委員の方にワークの被験者になっていただき、実際にやってもらう機会があったんです。そこで、あまりに「形式手法を書く」というお題と「実際に検証する」お題での食いつき方の違いに正直ビビりまして・・・（オンラインでの実験で顔が見えていなかったのにもかかわらず、目の輝きが違うのがわかりました。ええ、わかりました。）
結果、「これ、wacate（テストの勉強会）で発表するんだったわ」と原点にもどることができまして、検証の部分を厚くすることにしました。
他にも「班に積極的に回って説明を繰り返す」「解答をワーク中に配る」などいろいろいろいろ工夫はしてみました・・・。
補足（という名のいいわry）
今回、あまり導入を書かなかったので、「なぜ形式手法のセッションなんだ」っていう声が多く聞かれまして。。。
今回、テストとはちょっと離れた話題であったため、この「なぜ形式手法のセッションなんだ」という問いも質問者の立場によって意図するところがだいぶ違い、答えるべき答えも実はだいぶ違うんだなというのは自分の気づきとしてありました。
気づきとして、確かにあったのですが、これはブログという名の言い訳なので、好きなことを書きます。
- （テストエンジニアにとって）形式手法はなぜ必要か
それは、テストとは違ったアプローチでの品質へのアプローチを知ることで、視野を広げることができるってとこじゃないでしょうか。テスト7原則で「原則3.早期テストで時間とコストを節約」とありましたが、これはテスト以外の手段で開発の早い時期に品質を向上させるためのアプローチであり、考え方とかを知っておくのはとてもよいと思います。というか、そういうものがあることは絶対しっといたほうがよいです。
なお、個人的には、形式手法誕生の流れが「テストにはバグをなくすことができないが、形式手法ならバグのない仕様をつくりこめる！」っていう、ガチでテストに喧嘩を売って誕生した流れだったらしいあたりがとても面白かったです。
（念のためにいっときますけど、バグのない仕様を作れる保証はやっぱりないです。中世の「賢者の石」に係る化学の発展に似てますね！） - （テストエンジニアにとって）設計の手法とか必要なのか
なんだか「テストエンジニアにとってプログラミングは必要なのか」って命題と似てますね。プログラミングもそうですが、設計の手法を知らないと、おかしな挙動を発見しても、うまくバグを見つけ出したり、伝えたりしてあげられないってことが起こると思われます。ここについてはもっと書きたいことがあるのですが、もう疲れたのでまたの機会にします。 - （このワークのお題程度で）形式手法は必要か
まあ、あまり書こうとは思いませんね・・・。すみません・・・。 - （どんなシステムなら）形式手法は必要か
現在形式手法でよく言われているのはモデル検査ツールであるところのSPINらしい（と思っている）のですが、マイクロサービスとかAPI化の流れで並列処理を行うことができる機能が増えていくと、網羅的に仕様を確認できるモデル検査とかができるととても幸せになれると思います。また、VDMなどですと、これまた計算処理がとてもとても複雑かつ厳密である必要のあるシステム（金額計算がからむなど）では使うと、仕様をしっかり書き表せ、検証もできるということで、幸せになれると思います。
（こっそりとしか使ったことがなくて、具体的でなく、ごめんなさい。。）
感想
今回、説明しやすいワーク題材を考えるため四苦八苦した結果、さんざん「話さない」と言ってた、モデリングの抽象化とか捨象とか段階的詳細化とかそういうのがだいぶ自分としては体になじんだ気がします。と同時に、自分が今まであまりモデリングできてなかった事実に愕然としました・・・。
※もしかすると、自分にとっては絵じゃないほうがかえって抽象化・捨象がわかりやすかったんじゃないかと思ったのですが、もう眠いのでまたの機会。。
最後に
いろいろ不格好なセッションだったかとは思いますが、最初からの歩みを鑑みるに、ここが到達点の近似値であっただろうという意味において、後悔がないのが自分としての救いです。本当にレビュー等してくださった皆様がいなければどうなっていたか・・・。本当にありがとうございました。
そして、参加者の皆様、本当に聞いていただいてありがとうございました。
※関係ないけど今回のセッションのイメージ。お題が今回のセッションと似てるなとふと思い出してから、頭から離れなくなってしまいました。。改めて聴くとただの中二病ですね・・・。
