こんにちは、SWETの鈴木穂高（@hoddy3190）です。

コロナウィルスの影響で当初予定していた2020年3月4日（水）のDeNA TechCon 2020は中止になってしまいましたが、「せっかく資料も作ったしどうしてもDeNAのチャレンジを紹介したいんだ！」ということで、先週2020年3月12日（木）に一部のセッションをライブ配信しました。

タイトルにもある通り、私もゲームの仕様に関するテーマでライブ発表をしましたが、本記事はそのフォローアップということで、スライド資料の補足情報といただいた質問への回答を記載します。

発表内容

タイトル

仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ

f:id:swet-blog:20200317150044p:plain:w120

セッション情報

https://techcon.dena.com/2020/session/10

資料

仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ【DeNA TechCon 2020 ライブ配信】 from DeNA

動画

https://youtu.be/eKU5HOAtJsw?t=498

登壇者

今回は2名での発表でした。

鈴木穂高（@hoddy3190）
- スライドの1章から4章を説明
Kuniwakこと国分佑樹（@orga_chem）
- スライドの5章とまとめを説明

それぞれのプロフィールは、DeNA TechCon 2020のセッション情報ページをご覧ください。

各章の意図

章立てはスライドp4に記載しています。

2章「アプリゲーム運用の現場」では、アプリゲーム運用の現場ではどのような問題がどのような背景で起こるのか説明しています。その後の3章「我々のチャレンジ」では、それを踏まえた上で問題解決に向けた我々のチャレンジを説明しています。 4章「形式仕様記述の紹介」・5章「具体例」では、チャレンジの技術的な手段として形式仕様記述の紹介をしています。

今回はアプリゲーム運用の現場の説明や、形式仕様記述をやろうと思った背景の説明に、40分の発表のうち約半分の時間を費やしました。2章から3章、4章の一部が該当します。なぜそこまでの時間を費やしたのか。それは2019年8月末に行われたbuilderscon tokyo 2019の時も今回と似たような構成で発表したのですが、そのときの反省点からです。 builderscon tokyo 2019での発表の反応(togetter)も決して悪くはなかったとは思っていますが、中には形式仕様記述の必要性について疑問がぬぐえなかった方もおられたようです。builderscon tokyo 2019のときは発表時間が20分しかなかったことも大きいですが、形式仕様記述を試用するに至った背景を十分に説明しきれていなかった、というのが大きな反省点としてありました。解決したい問題があって初めて使う技術を選択できると思うので、形式仕様記述を試用するまでに至ったそのプロセスの共有はとても大事だろうということで厚く時間を割きました。

5章では具体例を用いてAlloyで形式仕様記述をどのように行うのかを説明しています。初めての方でもなるべく理解できるようにというのを前提に作りました。ただAlloyは書き方、考え方が手続き型のプログラミングとは異なるので、多くの人にとって初見で理解するのは難しいということは承知していました。なので、この章のメインテーマを「Alloyの書き方」ではなく、「いかに仕様の漏れを形式仕様記述で埋めていくか」にしました。一方で形式仕様記述をやったことがある人にとっては面白みのないものになる懸念があったので、先んじて形式仕様記述のテクニックを紹介するブログ記事を公開し、発表内でそのリンクを紹介する形をとりました。

今回の発表に対するTwitter上の反応をtogetterにまとめました。肌感としては、builderscon tokyo 2019のときと比べ、「わかりやすかった」という反応が増えたように思います。暗黙知をできる限り潰し、伝えたいことを解釈の幅をおさえて伝えるということが前よりはできたのかもしれません。

質問・回答

本発表への質問とそれに対する回答です。ライブ中に答えた質問も含め、Twitterや社内Slackなどで目に入った質問はすべて取り上げています。なお質問の文言は、意味がなるべく変わらないように整えた上で掲載しています。本記事とライブ配信で回答内容に齟齬がある場合は、本記事を正とさせてください。

Twitterでの質問

#denatechcon 無用な機能追加だったかどうかって事前にわからないのではないだろうか　A/Bテストとかしないと
— Fumikazu Fujiwara (@freddiefujiwara) March 12, 2020

こちらはスライドp46「無用な大規模化や無用な複雑化は避けるべきと考える」対する質問かと思われます。おっしゃるとおり無用かどうかを事前に見極めるのは難しいだろうと考えています。補足スライド内の記述ということもあり、この文言の意図としては「要求を満たす仕様の中で、もっと単純な選択もあるのにわざわざ複雑になるような仕様を選んでしまう必要はない」くらいのニュアンスで書いていました。仕様にまつわる問題は、今回我々の取り上げた「仕様が書かれない問題」以外にも様々あることがわかっています。本当に必要な仕様なのかどうかの結論づけをいかに行うかというのもそのひとつだと思います。ただ残念ながら現時点で我々もこうすれば良いだろうという具体的な案を持ち合わせているわけではないです。

”関係"は"有向"ですか？#denatechcon
— Ryosuke (@ryosukeeeee_) March 12, 2020

有向です。

initial commitはどうなるんだろう#denatechcon
— Ryosuke (@ryosukeeeee_) March 12, 2020

こちらおそらくInitial Commitの説明の前に発言されたものかと思われます。仕様作成者がInitial Commitの仕様に気づけておらず仕様書に明文化されていなかったが、Alloyで形式仕様記述をする過程を経てその仕様に気づけるという例をお見せしました。

仕様はAlloyをそのまま使うのではなく、自然言語にフィードバックするのかな？#denatechcon
— しましま(偽) (@shimashima35) March 12, 2020

仕様分析サポートチーム以外にどのような形で共有するかは現在検討中です。

単純に考えて、仕様追加のたびに組み合わせが増えるので組合せ爆発で検査に時間がかかりすぎる問題とかは出たりしてないのかな？

#denatechcon
— nakamura244 (@nakamura_244) March 12, 2020

おっしゃる通り、その問題は起きえます。 Alloyの場合は、小スコープ仮説（モデルの不具合のほとんどは小さい例で示せる）に基づき代表的な状態のみに絞って検査をしています。また我々が考えている対策案としては、形式的に記述した仕様を定理証明ツールで使えるような形に変換することを考えています。

形式手法から、正しさの証明されたロジックを各言語でexportまでできるとより良くなる可能性ないかな？（自分が知る限りそこまでしてくれるツールはないという理解）。その辺りに何か課題があるのかな...

#denatechcon
— nakamura244 (@nakamura_244) March 12, 2020

Alloyにはそういうexport機能はありませんが、export機能があるツールはいくつかありまして、例えばVDMToolsにはC++やJavaに変換する機能があるようです。

今回の仕様記述に（他のツールでなく特に）Alloy を採用した理由があれば知りたい。比較の結果でしょうか？ #denatechcon
— チェシャ猫 (@y_taka_23) March 12, 2020

我々が初めて形式仕様記述したプロダクトはOyakataです。

当時は形式仕様記述がどのようなものなのかぼんやりとしたイメージしか持っていなかったので、Oyakataの仕様を形式記述する動機は「Oyakataに貢献する」よりも「技術を知る」の方が大きかったです（cf. builderscon tokyo 2019「形式手法を使って、発見しにくいバグを一網打尽にしよう」p33）。 VDM++、Event-Bなど調べましたが、視覚的なフィードバックの得られるAlloyが初学者にとって易しそうだという理由でこの時はAlloyを選びました。

ちなみに、スライドp88に、「現在はOyakataの形式仕様記述を終えアプリゲームに適用している」旨を書いていますが、アプリゲームの仕様記述にはAlloyを用いていません。Oyakataへの形式仕様記述を通して、Alloyのメリット・デメリットがある程度把握できた上での判断です。こちらに関してはまたいつかお話できればと思っています。

社内からの質問

アプリゲーム以外でも形式手法による開発効率アップは見込めるでしょうか？

はい、見込めます。というのも、形式手法を適用してバグの件数が大きく減ったという事例は欧米を中心に多く報告されていた（航空宇宙、鉄道、電力など高い信頼性が必要とされる分野での事例が多い）ので、それをアプリゲーム運用にうまく適用できないだろうかと考えました。事例は形式手法の実践ポータルがよくまとまっていると思います。

形式手法のコスパ見極めはいつ完了しそうな見込みでしょうか？

アプリゲームには2019年の11月から適用をしていますが、1年以上はかかると思います。

仕様分析サポートチームは現在何人ですか？

4人（うちフルコミットは2人、あとの2人は兼業）です。4人で1つのプロダクトに形式仕様記述を適用しています。ネットや書籍に情報が少なく、手探りなことが多いので、モブプロを活用しながら取り組んでいます。

昨年のDeNA TechCon 2019とのつながり

昨年のDeNA TechCon 2019でKuniwakが発表した「ある SWET エンジニアの開発プロセス改善最前線 / Story of a SWET Engineer」でも形式手法、形式仕様記述を用いた取り組みについて発表しました。この時期は色々と種類がある形式手法の中でもモデル検査について調査していました（詳しくは、「ある SWET エンジニアの開発プロセス改善最前線 / Story of a SWET Engineer」のp87以降をご参照ください）。しかし会社の課題は何なのか、適切なアプローチは何なのかを改めて整理すると、形式仕様記述の方が適切そうだという結論になり方針転換をしました。そうした紆余曲折を経ながらも、現在ではOyakataをはじめ様々なプロダクトに適用するまでに至り、可能性を見極めています。まだまだ先は長いですが、これからも継続してチャレンジしていきます。