ゼロから学んだ形式手法

2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek（@takasek）です。

仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています（形式手法 カテゴリーの記事一覧）。

この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。

形式手法を学ぶ前の認識と疑問

ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造（モデル）を与え、そのモデルを解決の機構に落とし込む行為といえます。 その興味の延長線上で、よりアカデミックな裏付けのあるアプローチが取れると聞いて興味を持って形式手法を学び始めた私ですが、形式手法の概要を知った段階での認識・疑問は次のようなものでした。

そもそも「形式」「形式手法」の正体が掴めていない

形式手法というのはテストよりも抽象的に、網羅的に問題を発見できるらしい。

なるほど、たしかにテストの7原則によれば「テストは欠陥があることは示せるが、欠陥がないことは示せない」。その弱点をカバーできるとしたら形式手法はすごい。ただ理屈がよくわからない。書かれていないものは書かれていないのだから見つけようがないのでは？

形式手法は数理論理学に基づいているという説明もある。わからない。普段のプログラムだってif文を書くぞ。何が違うんだ。形式化されているのが違う？　なるほど……なるほど？　そもそも形式化って何だ？　プログラムのコードは機械が読むためのものだが、それは形式化じゃないのか？　やっぱりわからない。普通のプログラミングと形式手法を隔てるものは何なんだ？

形式手法の分野の違いがわからず混乱する

形式手法の分野には主に「形式仕様記述」「モデル検査」「形式検証（定理証明）」があるらしい。

しかし字面から違いがよくわからない。形式仕様記述は記述するだけで検査や検証をしないのか？　仕様とモデルの違いは？　検査と証明・検証の違いは？　混乱する。しかも各分野の中にもツールがたくさんあるようだ。なんでそんなにたくさんあるんだ。統一してほしい。

数学をちゃんと学ぶ必要があるらしいが、本当か？

そりゃ何事も学ぶほうがいいのはわかる。たとえば仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blogには以下のような記述が登場する。

存在量化子というやつだ。なるほど。こういう概念が登場したときに数式が理解できないとたしかに困りそうだ。でも、そういうテクニックだけをピンポイントに使う形でカバーできないのだろうか？

これまで触れてきたプログラム言語の型付けでも、存在型（existential）や全称型（generics）が登場する。基礎から理論を理解できるならもちろん良いが、とりあえず表面だけでもなんとかごまかしごまかし使うことができている。

形式手法も実はごまかしでいける部分が存在するのでは？　要求レベルを上げていったらきりがないじゃないか。「学ばないと太刀打ちできない」というような言い回しは不当にハードルを上げているだけでは？　それとも形式手法の場合には決定的に「数学を学ばないと太刀打ちできない」ような事情があるのだろうか？

実際どこまで役に立つのだろうか

正直、知的好奇心に駆られて転職しちゃったところがあり、実際にプロダクト開発の現場で汎用的に適用できるイメージは具体的に湧いていない。

「形式手法の実践ポータル」に事例がまとめられているが、大層なプロジェクトばかりだ。現状、普通の開発現場で形式手法が流行っている様子はない。ということは、適用範囲がけっこう限られるのでは？　どれくらい汎用性のある技術なんだろうか？

今の理解

このような疑問を持ちながら3か月の学習と実践を重ねていった結果、現在は以下のような理解に辿り着きました。

「形式」は証明のためのスタートライン

私の当初の「プログラムのコードだって形式化されているのでは？」という疑問は正解です。普段プログラマが使うプログラム言語は形式言語です。利用可能な文字集合、文法のルールが規定されており、曖昧な構文を許さない言語です。

形式手法と普段のプログラムと違う点は数理論理学に基づく点だと言われます。だから網羅性があり、テストでは発見できないような欠陥も発見できる。……よくわかりませんね。何が違うのでしょうか。

実は誰でも同様のアイデアを昔習ったことがあるはずです。私も中学数学の復習をしたら分かりました。証明です。

三平方の定理を考えてみましょう。a,bの二辺と長さcの斜辺からなる直角三角形においてa²+b²=c²が成り立つという定理です。

この結果を確認したいとき、プログラマが慣れているユニットテストでは具体的なケースを列挙するしかありません。 {a:3, b:4, c:5} のとき成り立つ、 {a:5, b:12, c:13} のとき成り立つ……といったように。Property Based Testingであれば大量のランダムな入力を与えることも可能ですが、どこまでいっても有限個の試行の繰り返しです。

しかし証明なら、個別のケースではなく任意の無限の直角三角形について定理が成り立つことを示せます。中学数学の証明では、直角三角形の図に補助線を引くなどの作業を通じて、すでに明らかな定義を変形させて定理を導きました。

中高の数学の範囲を離れると、次のように言えます。無条件に正しいと見なせる命題を公理といいます。公理に繰り返し推論規則を適用していくと定理を導出できます。その論理の筋道をつけるのが証明です。

形式手法の話に戻ります。形式手法とは「このシステムは正しい」と言えるようにするための手法です¹。言い換えると、命題「このシステムは正しい」を証明するのが形式手法のゴールです。そして数学的な意味で証明可能にするためには、漠然とした「正しい」を数理論理学の世界に持ち込まなくてはなりません。

自然言語で書かれたシステムの仕様には曖昧さがあり、機械的な推論規則の適用もできません。それでは証明などできません。形式言語を使って論理式として仕様を表現することが、形式手法のスタートラインです。

形式手法の分野は多岐にわたり、また横断的である

システムの正しさを証明するのが形式手法のゴールだと述べました。形式手法の分野の違いは、その筋道のつけかたの違いです。

形式手法の多くは次のような二側面を持ちます。

• システムのある性質を表現する仕様を形式的に記述し、
• なんらかのツールを通じて検査・検証にかけ、結果を出力する

この前者および後者のバリエーションがさまざまな形式手法の違いです。

まず対象のシステムとは何かを考えてみましょう。システムと一言で言っても、入力と出力が1対1で対応するシステムと、異常がない限り動き続けてイベントを待ち受けるシステムは別物です。複雑な内部状態と条件分岐を持つゲームも、独立動作し協調しあう分散システムも「システム」です。

システムの中でも、検証すべき性質はひとつではありません。性質に応じて出力の形は変わります。

• 仕様を詳細な設計に落としたとき、不正な挙動が混入していないことを確認したい
• システムを構成する複数のコンポーネントの関係について、可能なパターンをグラフィカルに図示したい
• 具体的なシナリオに沿って、状態遷移をシミュレーションしたい
• 並行システムの挙動を合成して、不具合が起こりうるケースを網羅的に検知したい
• 複雑な証明の途中式を自動的に補完しながら巨大な証明を完成させたい

こういった異なる目的を、同一の手法・ツールでは達成できません。

形式化のベースとなる論理体系も一様ではありません。たとえばアルゴリズムが仕様を満たしていることを検証したければ、その事前条件・事後条件をHoare論理を使って記述します。システムの長いライフサイクルにおける性質を検査したいときには「いずれtrueになることがある」「常にtrueのまま」といった時相論理を使った表現を使うこともできます。他にも検証したい性質に応じて、門外漢には想像もつかないほど多様な論理体系が存在するようです。

ただし強力な表現ができるほどよいというわけではありません。必要十分な表現力があればよいのです。記述の自由度と解析の簡単さはトレードオフです。無用に記述が複雑すぎると理解しづらくなり、仕様記述に矛盾や不整合がないことの検証（verification）のみならず「その仕様は本当に問題の解決の形として妥当か」の確認（validation）に支障が出ます。またシステムの全状態をモデルとして表現して網羅探索するモデル検査では、詳細すぎるモデルは状態爆発により現実的な時間内での検査が難しくなります。重要なのは適切な抽象度での仕様記述・モデリングです。時には表現力を制限し簡単な記述を可能にしたDSL（ドメイン特化言語）が有効な解決策になります。

ソフトウェア工学の道具としての形式手法では、形式手法とは何かという問いに、次のような説明で答えています。

数理論理学に基づく言語ならびに証明技法などからなる基礎理論を持つことに加えて、設計手法、ドメイン知識、などが関係する総合的な技術²

形式手法と一言で言おうとしても輪郭が掴みづらいのは、そういった総合的な側面が影響しているのでしょう。

先述したとおり形式手法には「形式仕様記述」「モデル検査」「形式検証」があると言われますが、3つの分野を排他的なものとして考えると混乱します。モデル検査であろうと形式検証であろうと仕様記述は必要です。たとえば代表的な形式検証のツール（定理証明系）であるCoqの記述言語Gallinaも、明確に「仕様記述言語」だと説明されています³。

今私たちが取り組んでいるプロジェクトでも、目的までのロードマップには3分野いずれの技術も必要になっており、いくつもの手法を組み合わせて活用しています。何かひとつのツールを触って理解した気になるのではなく、問題に対して適切な抽象度とツールを選ぶために見識を広げていかなければならないと思います。

形式手法にとって数学は基礎的な語彙である

形式手法のツールには、難しい理論を知らずとも扱えるようにデザインされているものもあります。たとえば当ブログのDeNA TechCon 2020の発表についての記事で述べたように、仕様分析サポートチームでは当初「視覚的なフィードバックを得られるので初学者に易しい」という理由でAlloyを採用しました。ツール上でフィードバックを得ながら試行錯誤していたらなんかうまいこと目的達成できた、という体験も悪くはないでしょう。

しかし形式手法に正面切って向き合うなら、表層だけ撫でる態度はむしろ効率を損ないます。先に述べたように、あるシステムの仕様を適切に記述し性質を検証・検査可能にするためには、どのみち形式仕様記述を避けて通れません。モデル検査は「ボタン一発の検証法⁴」とは呼ばれますが、そのモデリングのためには抽象化技術が必要ですし、検査結果を読むにあたっても論理学の理解がないとしばしば誤った解釈をしてしまうそうです。数理論理学は形式手法での読み書きを支える基礎的な語彙となります。

そして論理学は、概念の積み上げで成立しています。注意深く足を進めないとすぐ転んでしまいます。例をいくつかご覧に入れましょう。

述語という単語を耳にしたとき、論理学の素養がない人は「主語でない文節」と理解することが多いでしょう。すると論理学での「変数を含み、変数に具体的な値を代入することによって真偽が定まる叙述⁵」という理解ができなくなります。

当記事でも何度も言及している性質は、数理論理学の世界では「変数が1つの述語」です。あなたのイメージと合致していたでしょうか？　この理解は普段の日本語やオブジェクト指向に慣れ親しんだプログラマからは距離があります。

ときには普段のプログラミングでの考え方が邪魔をすることすらあります。形式仕様記述にもいくつかのアプローチがありますが、私が現在取り組んでいる仕様記述は状態に注目するモデル規範と呼ばれる方法なので、その話をしましょう。

ここで状態というのは「局所状態の掛け合わせとして立ち現れた、システム全体のグローバルな状態」です。プログラマは普段、グローバルな状態は悪だと考えているものです。なるべく状態を局所に留め、モジュール内の状態は隠蔽するよう、半ば教条主義的に訓練されています。なのでグローバルな状態という存在を受け入れるには、私にとってはかなりの発想の転換が必要でした。

モデル規範の形式仕様記述では、すべての状態の集合から特定の状態を取り上げ、状態どうしの関係を記述することになります。この手順を飲み込むまでにも時間を要しました。普段プログラマは多かれ少なかれパフォーマンスを気にしながらコードを書いています。もし集合（Set）に数万の要素が入ると言われたら、ぎょっとしてアルゴリズムを考え直すことが多いでしょう。グローバルな状態の集合は、天文学的な要素数をものともしません⁶。そういうものを扱う数学的な発想に、私は最初大きく戸惑いました。

「すべての状態」があらかじめ存在しているという前提を受け入れると、パラダイムが大きく変わります。事前状態・事後状態の関係は pred hoge(s, s') のように記述します⁷。日頃プログラマとして慣らされているような「事前状態を具体的な引数として受け取り、加工して事後状態を返す」関数ではなく、時間経過を伴わない静的な記述だというのがポイントです⁸。

このように形式手法を学ぶ中ではしばしば、日常用語と異なっていたり、これまでのプログラミングの延長で捉えられない概念に遭遇します。既存の枠組みに引き寄せて歪んだ理解に辿り着かないよう、注意深くならなければいけません。

定評のある数学の教科書はどれも、まず単純な定義から始め、定義済みの確かなものを積み上げると新たな概念が獲得されるように書かれています。私のような現場でのアドホックな学習で育ってきた人間は、基礎を積み上げていくアカデミックな手続きをおろそかにしがちです。最初から数学やってる人には丁寧な手続きが常識なのかもしれませんが、少なくとも私はそういう足腰が弱ってることを自覚しないとすべてが始まりませんでした。

問題を分割統治するのはプログラミングでも散々やってきたはずだし、場合分けして分割統治、各個撃破というのは中学高校の証明で習ってるはずなのに、大人になると忘れちゃうし身についてないんですよね。不思議ですね。

形式手法は役に立つ！

かつて形式手法は、システムのすべての性質を壮大な論理体系で表現し、厳密な仕様がそのまま動くプログラムへと詳細化される世界（Correctness by Construction）を夢見ていました。しかしそれは壮大すぎて難しく、今世紀に入ってからは実用性を意識する Formal method Light が主流となったそうです⁹。

プログラマが日常的に頼っている型システムも「型システム入門」によれば「最も確立された軽量形式手法」¹⁰です。当初の私の認識「普通の開発現場で形式手法が流行っている様子はない」なんてとんでもない勘違いでした。もう当たり前のように、形式手法はソフトウェアエンジニアリングの世界に溶け込んでいるのでした。

デザイン電卓として

かつてモバイルアプリエンジニアとして携わった案件でも、今と同様の知識があれば形式手法の実践を検討しただろうと思える局面が何度かあります。

私があるとき設計・実装したのは、端末のオンメモリ・サーバ通信・永続化層・さらにアプリバージョンのアップデートといった複数の状態が非同期に絡み合う複雑な機能でした。人数と時間をかけて何度も仕様をチェックし設計しましたが、やはり多くの細かいミスが出ました。テストを書いても「本当にこれですべて確認できるのか」「テスト自体が間違っているのでは」という不安がつきまとい、実際その不安は大いに的中しました。転ばぬ先の杖として不正なデータを差し戻す処理を随所に入れたりもしましたが、本当にそれが必要なガードだったのか、もしくは無用に仕様を複雑にしただけなのかは今でも分かりません。

今の自分が当時に戻ったら、この案件に限って形式仕様記述してモデル検査にかけよう！　と提案することでしょう。モデルが正しく振る舞うことを早期に検査できれば安心して開発を進めることができます。目的を絞ればそこまでの導入コストはかからず、十分ペイするはずです。

このように、大がかりにではなくアドホックな形で形式手法を用いるアプローチは「デザイン電卓」と形容されるそうです¹¹。形式手法に対しての大仰なイメージを払拭してくれる素敵な表現だと思います。

仕様の妥当性確認として

メリットは、ツールによる正当性（correctness）の検査（verification）だけではありません。形式的に仕様記述すること自体が「その仕様は本当に問題の解決の形として妥当か」の確認（validation）となります。

普段のソフトウェア開発業務で仕様書を読み書きするとき、条件の不明瞭さや期待結果の曖昧さ、項目どうしのつながりに不安を覚えることはないでしょうか。私はありました。自然言語の表現力に絶望して、おもむろに擬似コードを書き始めることもありました。頭の中ではなんとなくうまくいきそうなのに、条件の漏れやブレによって適切な仕様化に失敗することはよくあります。そんなとき、形式言語は仕様の妥当性を厳密に確認するための、まさに言語として役立ちます。

先日のDeNA TechConでの発表では、この側面について詳細に解説しています。予備知識がなくともわかりやすい発表になっていますので、是非あわせてご覧ください。

DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました（録画・スライドあり） - DeNA Testing Blog

より積極的な適用として

ソフトウェア開発のプロセスは、ある入力を別の形へと変換して出力する作業の繰り返しといえます。変換の中で混入した誤りが、後で致命的なバグに成長します。形式手法を活用すれば、そんなときに前後の入出力、あるいは別の変換を経た複数の成果物が同じ意味だと保証できるのです。これは非常に汎用的かつ強力なアイデアです。一度習得した技術が開発プロセスの至る所で使えるというのは、夢が広がりますよね。

私たち仕様分析サポートチームはそのような考えのもと、積極的に形式手法の活用局面を探っています。

おまけの副産物

形式手法の土台には多くの数学的背景が横たわっています。これはコンピュータサイエンスの土台でもあります。つまり形式手法を学べば必然的に、プログラミングの深い理解にも繋がります。

たとえば契約による設計は「オブジェクト指向入門」¹²でバートランド・メイヤーが唱えた概念ですが、その由来がHoare論理にあるのだと理解できました。

また、私はSwiftコンパイラ好きが集まるわいわいswiftc - connpassというイベントが好きでよく顔を出しています。そこでは発表のたびに「SwiftコードのコンパイルにはAST→Sema→IR→…というフェーズがあって」という説明が頻出します。この説明も「単にそういう手続きだ」というだけでなく「統語論と意味論を分けているのだな」と理論上の納得を得られるようになりました。

いろいろな技術領域を闇雲につまみ食いしていた私にとっては、バラバラだった知識に連続性がもたらされ、とても良い学びの機会となっています。

まとめ

人間はいい加減な存在です。自然言語の世界はなんとなく動いているように見えても、あちこちに誤魔化しや綻びがあります。たとえば「または」が排他的選言と両立的選言のどちらを示すかは文脈によるとか、「1日おき」の意味が曖昧だとか。でも我々は意識しないと曖昧さに気づけないものです。そんなあやふやな論理を扱う人間だから、一度日常の世界を離れて数理論理学の力を借りる必要があります。

形式手法は強力で信頼できる論理体系に支えられており、それでいて多種多様です。場合によっては親しみやすくもあり、思ったよりも汎用的な技術領域に感じられます。

そんな形式手法についての、今時点での理解について書き連ねてみました。私と同じように形式手法に対しての疑問を感じていた方への道しるべになれば幸いです。

今後もSWETでは形式手法の実用性を見極める研究を続け、アウトプットしていきます。よろしくお願いします。

---

1. 「ソフトウェア工学の道具としての形式手法」 p2 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩

2. 「ソフトウェア工学の道具としての形式手法」 p2 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩

3. The Gallina specification language — Coq 8.11.0 documentation https://coq.inria.fr/refman/language/gallina-specification-language.html↩

4. 「ソフトウェア工学の道具としての形式手法」 p12 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩

5. 「ソフトウェア科学基礎」p12 https://www.amazon.co.jp/dp/4764903555↩

6. 記述上無限を扱えるという話であって、網羅的にパスを辿るモデル検査時にはパフォーマンス考慮が必要なことはあります。↩

7. 具体的な記述の感触を掴みたい方は、仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blogもご参照ください。↩

8. 条件によっては「事前状態を引数として受け取り、加工して事後状態を返す」書き方に変換可能なことはあります。↩

9. 「ソフトウェア工学の道具としての形式手法」 p4 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩

10. 「型システム入門」p1 https://www.amazon.co.jp/dp/B07CBB69SS↩

11. 「ソフトウェア工学の道具としての形式手法」 p13 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩

12. 「オブジェクト指向入門　第2版　原則・コンセプト」 11章 https://www.amazon.co.jp/dp/4798111112↩

DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました（録画・スライドあり）

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

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

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

発表内容

タイトル

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

セッション情報

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をはじめ様々なプロダクトに適用するまでに至り、可能性を見極めています。 まだまだ先は長いですが、これからも継続してチャレンジしていきます。

さいごに

DeNA TechCon 2020のテーマは「Craftmanship」です。 問題解決のために私たちが技術を徹底的に磨きチャレンジを続けてきた様子を、会場にて直接皆様の前でお伝えできずに残念でしたが、 これからも定期的にSWET Blog等を通じて発信していきますのでよろしければご覧ください。

また、DeNA TechConをはじめ、DeNAエンジニアの登壇お知らせや彼らが書いたブログ記事等の紹介をTwitterアカウント（@DeNAxTech）にてお届けしています。ぜひフォローをお願いします！

Follow @denaxtech

Golden TestではじめるGoのAPI ServerのRegression Test

はじめに

昨年（2019年）の11月にSWETチームへJoinした伊藤（@akito0107)です。 SWETチームでは主にGoのサービスに対するテスト実装のサポートや品質向上の取り組みを行っています。

この記事では、GoのAPI ServerのRegression Testについて、その目的と低コストに始められるGolden Files を使ったテスト手法をサンプルのコードを交えながら紹介しようと思います。

API ServerのRegression Test

Goに限らず、サービスの成長に伴い常に変更が入るようなシステムだと、過去に実装したアーキテクチャが現在の仕様に適さなくなるといったケースも多くあると思います。 そういった場合、Refactoring、Rearchitectingなどを行い、より理想の形へソースコードやアーキテクチャを進化させていきます。その際に重要なのが、 過去の仕様と変更がないこと を保証するということで、Regression Test（あるいは回帰テスト）はこれを目的にしたテストです。

httpのAPI Serverにおける 仕様と変更がないこと の保証とは、極端に単純化して言うと同じhttp requestを同じ条件（時間・パラメータなど）で投げたときに、同じhttp responseが返ってくることを保証することです。 この記事では、この定義でRegression Testを扱って説明をしていこうと思います。

Golden Test

過去に実行したテストの結果をファイルに保存（= Golden Files）し、再度実行するときはそのファイルと同じ結果が返ってきているかどうかをチェックするテスト手法のことを Golden Test と呼びます¹。 Advanced Testing with Goで紹介されていますが、簡単に動きを見てみましょう。 以下の擬似コードを見てください。

var update = flag.Bool("update", false, "update golden files")

func TestDoSomething(t *testing.T) {
  // Test対象の関数をCallする
  result := DoSomething()
  golden := filepath.Join("/path/to/testdata/", t.Name() + ".golden")

  // update flagが指定されていた場合はfileを書き出す
  if *update {
    ioutil.WriteFile(golden, result, 0644)
  }

  // golden fileを読み込む
  expected, _ := ioutil.ReadFile(golden)
 
  // 変更がないかをチェックする
  if bytes.Equal(result, expected) {
    t.Errorf("golden file not matched")
  }
}

このテストでは、 DoSomething() のチェックを行っています。 DoSomething()からの返り値をそのままファイルに書き出し、 bytes.Equalを使ってファイルの値と実行した値が同じかどうかを比較しています。 暗黙的にDoSomething()の返り値が[]byteであることを想定しているのに注意してください。

ポイントとしては、 -update フラグを設定した際に、書き出したGolden Filesをupdateするというところです。 もちろんAPIに仕様変更があった際にはoutputが変わるのは当たり前なので、この-updateフラグのようなGolden Filesのメンテナンスを容易にする仕組みを取り入れましょう。

今回はgoldieというライブラリを使って Golden Testを行っていこうと思います。-updateフラグでGolden Filesをupdateする仕組みなどは上記のコードと変わりませんが、jsonでの比較やdiffが出た際のvisualizeなどが作り込まれていて、便利に使うことができます。

Golden Filesを使ったAPIのRegression Test

では、goldieを使ってRegression Testを書いて行きましょう。

Goldieの使い方

goldieの使い方を簡単に見てみます。 なお、goldieはv2.2を使います。 v1とv2ではAPIが違うので注意してください。

go getを使ってinstallします。この際にv2を指定します。

$ go get github.com/sebdah/goldie/v2

実際にgoldieを使う際にはNewで初期化したあとに、Assertを呼ぶだけです。 試しに上のコードをgoldieを使った形に直してみましょう。

func TestDoSomething(t *testing.T) {
    result := DoSomething()

    // goldieを初期化
    g := goldie.New(t)

    // Golden Fileとの比較
    g.Assert(t, t.Name(), result)
}

goldie自体でupdateフラグによるGolden Fileのメンテナンスなどをサポートしてくれます。

また、Golden Fileと比較するAssertという関数は3種類あり、ユースケースに応じて呼び分ける必要があります。上の例で使ったAssertは[]byte同士を比較します。ほかにも、JSON同士を比較できるAssertJsonや、Templateを使って実行時に動的に値を書き換えられるAssertWithTemplateがあります。

goldieではデフォルトで、testdata配下にGolden Fileが保存されます。このPathを書き換えたいときは、WithFixtureDirのOptioinをNewに渡します。

   g := goldie.New(t, goldie.WithFixtureDir("./testadata/golden"))

このケースだと./testdata/golden配下にファイルが保存されます。

それ以外にも多くのオプションがあるので、GoDocを参照してみてください。

API ServerでのExample

では、goldieを使ってAPI ServerのRegression Testを書いていきます。

下記のようなHandlerを持つAPIを想定してテストを書きます（error handlingなどのコードは一部省略しています）。 emailとnameの値を受け取り、DBに保存するというユースケースのAPIです。

// User定義のstruct
// ID / CreatedAtはDBにより自動でセットされる想定
type UserJSON struct {
    ID        int       `json:"id" db:"id"`
    Name      string    `json:"name" db:"name"`
    Email     string    `json:"email" db:"email"`
    CreatedAt time.Time `json:"created_at" db:"created_at"`
}

type ErrorResponse struct {
    Message string `json:"message"`
}

// Error用関数
func writeError(w http.ResponseWriter, message string) {
    w.WriteHeader(http.StatusInternalServerError)
    json.NewEncoder(w).Encode(&ErrorResponse{Message: message})
}

func postUser(db *sqlx.DB) http.HandlerFunc {
    return func(w http.ResponseWriter, r *http.Request) {
        // JSONのbinding
        var body UserJSON
        if err := json.NewDecoder(r.Body).Decode(&body); err != nil {
            writeError(w, "json decode failed")
            return
        }

        // DBへInsert
        ctx := r.Context()
        rs, err := db.ExecContext(ctx, "INSERT INTO users(name, email) VALUES (?, ?)", body.Name, body.Email)
        if err != nil {
            writeError(w, "insert user failed")
            return
        }

        // IDはAuto IncrementでAuto Generateされるので、その値を取得してくる
        id, err := rs.LastInsertId()
        if err != nil {
            writeError(w, "last insert id failed")
            return
        }

        // Response用にDataを取得する
        var user UserJSON
        if err := db.GetContext(ctx, &user, "SELECT * from users where id = ?", id); err != nil {
            writeError(w, "get user failed")
            return
        }

        // Responseを返す
        w.WriteHeader(http.StatusCreated)
        if err := json.NewEncoder(w).Encode(&UserJSON{
            ID:        user.ID,
            Name:      user.Name,
            Email:     user.Email,
            CreatedAt: user.CreatedAt,
        }); err != nil {
            writeError(w, "json encode failed")
            return
        }
    }
}

http.HandlerFunc を直接定義するのではなく、 http.HandlerFunc を返す関数として定義しています。このコードの例のように、 db 等の依存モジュールを外部から受け取れるようにするためです。このメリットは後にテストコードを書くときに体感できると思います。

main.go ではこの handler を下記のようにして読み込んでいます。

func main() {
    db := sqlx.MustConnect("mysql", "root:passw0rd@tcp(localhost:3306)/e2e_example?parseTime=true")
    defer db.Close()

    handler := postUser(db)

    if err := http.ListenAndServe(":8080", handler); err != nil {
        log.Fatal(err)
    }
}

今回はhandlerが1つなので、特にrouterのライブラリなどは使っていません。

この postUser ハンドラに対してテストを書いていきます。 テストとしては以下のような流れになります。

1. APIにhttp requestを投げ、responseをGolden Filesとして保存
2. テスト実行の2回目以降はresponseがGolden Filesと差分が無いかを確かめる

func TestPostUser(t *testing.T) {
    db := sqlx.MustConnect("mysql", "root:passw0rd@tcp(localhost:3306)/e2e_example?parseTime=true")

    t.Cleanup(func() {
        // Go1.14から導入された関数
        // DBにinsertしたdataのcleanupを行う。 キー制約を削除し、truncateする
        db.MustExec("set foreign_key_checks = 0")
        db.MustExec("truncate table users")
        db.MustExec("set foreign_key_checks = 1")
        db.Close()
    })

    var buf bytes.Buffer
    if err := json.NewEncoder(&buf).Encode(&UserJSON{
        Name:  "test",
        Email: "test@dena.com",
    }); err != nil {
        t.Fatal(err)
    }

    // httptestによりRequestとResponseRecorderを作成する
    req := httptest.NewRequest(http.MethodPost, "/", &buf)
    rec := httptest.NewRecorder()

    // http requestをsimulateする。 `rec` にResponseが書き込まれる。
    postUser(db).ServeHTTP(rec, req)

    if rec.Code != http.StatusCreated {
        t.Fatalf("status code must be %d but %d", http.StatusCreated, rec.Code)
    }

    // Response BodyのJSONをDecodeする
    var user UserJSON
    if err := json.NewDecoder(rec.Body).Decode(&user); err != nil {
        t.Fatalf("json Decode failed: %v", err)
    }

    // goldieの初期化
    g := goldie.New(t)

    // Golden Fileとの比較を行う
    g.AssertJson(t, t.Name(), user)
}

httptest を使ったシンプルな構成ですが、handlerの中でdbにつなげているので、dbをテストの中でもopenし、handlerに渡しています。

テストの後半にgoldieでAPIのresponseのJSONを比較しています。JSONの比較なので、AssertJsonを使っています。

このテストを動かしてみましょう。（DBはlocalhost:3306でlistenしている前提です） すると、下記のように出力されるはずです。

$ go test .
--- FAIL: TestPostUser (0.03s)
    e2e_test.go:42: Golden fixture not found. Try running with -update flag.
FAIL
FAIL    github.com/DeNA/apiexample  0.085s
FAIL

fixtureがないというメッセージでFailします。メッセージの通り、-updateをつけてテストを実行してみましょう。

$ go test . -update
ok      github.com/DeNA/apiexample  0.091s

今度は成功しました。また、testdataというディレクトリが作成されていることに気づくと思います。中に、TestPostUser.goldenというファイル作成されています。このTestPostUserというファイル名は今回実装したテストの関数名と同じでしたね。 goldie.AssertJSONの第2引数で渡しているt.Name()はTestPostUserなので、第2引数で渡した文字列の名前のファイルが出来ていることが分かると思います。

.
├── go.mod
├── go.sum
├── main.go
├── main_test.go
└── testdata
    └── TestPostUser.golden

TestPostUser.golden のファイルの中を見てみましょう

$ cat testdata/TestPostUser.golden
{
  "id": 1,
  "name": "test",
  "email": "test@dena.com",
  "created_at": "2020-03-06T03:50:31Z"
}

APIのresponseのjsonがそのまま保存されています。

この状態で、もう一度go testを実行してみましょう。

$ go test .
--- FAIL: TestPostUser (0.03s)
    e2e_test.go:42: Result did not match the golden fixture. Diff is below:

        --- Expected
        +++ Actual
        @@ -4,3 +4,3 @@
           "email": "test@dena.com",
        -  "created_at": "2020-03-06T03:50:31Z"
        +  "created_at": "2020-03-06T03:54:04Z"
         }

FAIL
FAIL    github.com/DeNA/apiexample  0.089s
FAIL

テストがFailしてしまいましたが、なぜFailしたのかの差分ををわかりやすい形式で表示してくれるのが、goldie を使う利点です。

created_at はDBへinsertするときにMySQLのCURRENT_TIMESTAMPで設定しているため、実行時の時間が挿入されます。そのため、実行ごとに値が異なってしまうため、API Responseの値に差分がでてしまいました。

実行時に値が変わる時の対処法

今回のcreated_atに変更があったケースですが、テストがFailしていることが間違っている状態、つまり偽陽性のあるテスト、となってしまっています。特に時間や、Auto GeneretedされるIDなどの値は実行時に変更されるため、Golden Testsで扱うのが難しい部類となります。ここでは、これに対応するパターンをいくつか考えていこうと思います。

外部からTimestampを取得できるようにする

DBの current_timestamp を使わずに、アプリケーション上でタイムスタンプを取得し、INSERT時に渡すように書き換え、その上でテストコードからタイムスタンプを取得するロジックを操作できるようにします。 dbと同じように関数の引数でタイムスタンプを取得する関数を渡すか、 プログラミング言語Go² 11.2.3ホワイトボックステストで触れられているような、関数をpackage scopeの変数として定義しテスト時に置き換えるような方法を取るかの2パターンが考えられます。 ここでは後者の方を採用し、実装してみたいと思います。

handlerを以下のように書き換えます。

+var now = func() time.Time {
+       return time.Now()
+}
+
 func postUser(db *sqlx.DB) http.HandlerFunc {
        return func(w http.ResponseWriter, r *http.Request) {
                if err := json.NewDecoder(r.Body).Decode(&body); err != nil {
                    writeError(w, "json decode failed")   
                    return 
                }

                ctx := r.Context()
-               rs, err := db.ExecContext(ctx, "INSERT INTO users(name, email) VALUES (?, ?)", body.Name, body.Email)
+               rs, err := db.ExecContext(ctx, "INSERT INTO users(name, email, created_at) VALUES (?, ?, ?)", body.Name, body.Email, now())

 ~省略~ 

nowという変数を定義し、INSERT時にその関数を使うようにします。 Testは以下のように修正します。

 func TestPostUser(t *testing.T) {
        db := sqlx.MustConnect("mysql", "root:passw0rd@tcp(localhost:3306)/e2e_example?parseTime=true")

+       saved := now
+       now = func() time.Time {
+               n, _ := time.Parse(time.RFC3339,"2020-03-03T15:04:05Z")
+               return n
+       }
+
        t.Cleanup(func() {
                db.MustExec("set foreign_key_checks = 0")
                db.MustExec("truncate table users")
                db.MustExec("set foreign_key_checks = 1")
                db.Close()
+
+               now = saved
        })

       ~省略~

テストの関数の中でnowを上書きし、任意の固定の時間を返すようにします。そのうえで、テストを何回か実行してみてください。固定の時間が使われるようになったため、テストが安定して動くようなりました。 t.Cleanup もしくは、deferなどで、テスト実行時に元の関数に値を戻すことを忘れないでください。もしその関数が他のテストに依存していた場合、値が食い違ってしまいます。

このパターンは時間など、実行時に依存する値をコントロールする汎用的なものです。もしAPI Server以外でも同じ様なケースで困ったら採用してみる価値はあるかもしれません。

Http Headerで時間を操作できるようにする

httpのAPI Serverに特化したパターンも考えてみましょう。httpのmiddlewareで時間を設定し、handlerの内部ではその値を使うようなパターンを実装してみます。

以下の様なmiddlewareを実装しましょう。　

const requestTimeHeaderKey = "X-Request-Time"
type requestTimeCtxKey struct{}

func requestTimeMiddleware(next http.HandlerFunc) http.HandlerFunc{
    return func(w http.ResponseWriter, r *http.Request) {
        now := time.Now()

        t := r.Header.Get(requestTimeHeaderKey)

        if t != "" {
            if n, err := time.Parse(time.RFC3339, t); err != nil {
                now = n
            }
        }

        ctx := context.WithValue(r.Context(), requestTimeCtxKey{}, now)
        r = r.WithContext(ctx)
        next(w, r)
    }
}

X-Request-Timeのhttpのrequest headerがあったら、その値をcontextにセットし、なければ、time.Nowを使います。

handlerでcontextからの値を使うように修正してみましょう。

func postUser(db *sqlx.DB) http.HandlerFunc {
                if err := json.NewDecoder(r.Body).Decode(&body); err != nil {
                    writeError(w, "json decode failed")   
                    return 
                }

                ctx := r.Context()
-               rs, err := db.ExecContext(ctx, "INSERT INTO users(name, email) VALUES (?, ?)", body.Name, body.Email)
+               now := ctx.Value(requestTimeCtxKey{}).(time.Time)
+               rs, err := db.ExecContext(ctx, "INSERT INTO users(name, email, created_at) VALUES (?, ?, ?)", body.Name, body.Email, now)

        ........

テスト側ではmiddlewareでhandlerをwrapし、headerをセットしましょう。

~省略~
+       req := httptest.NewRequest(http.MethodPost, "/", &buf)
+       req.Header.Add(requestTimeHeaderKey, "2020-03-03T15:04:05Z")
        rec := httptest.NewRecorder()

-       postUser(db).ServeHTTP(rec, req)
+       requestTimeMiddleware(postUser(db)).ServeHTTP(rec, req)
~省略~

これでテストを実行してみましょう。Failになることはなくなったと思います。 headerをセットする方法は外部から時間を操作できてしまい、意図しないリクエストを発行される恐れがあるので、テストでのみ有効になるように、build tagなどを使って調整することをおすすめします。

zero値に置き換える

上記2つの方法はアプリケーションコードに手を加える方法でした。ここでは、テストの方に修正を加えて、実行時に値が変わる項目に対応していきたいと思います。

goldieへわたす前に、値をzero値、もしくは固定値に書き換えてしまえばテストは安定します。

        ........
        g := goldie.New(t)
        var user UserJSON
        json.NewDecoder(rec.Body).Decode(&user)
+       user.CreatedAt = time.Time{}
        g.AssertJson(t, t.Name(), user)
 }

非常に乱暴なやり方ですが、今回のようにテスト時に無視できるとわかっている値がある場合には最もコストが少ない方法です（とはいえ、乱用してはテストの意味がなくなってしまうので注意深く使いましょう）。

reflectパッケージを使って、以下のような helper を実装しても良いと思います。

func ignoreField(t *testing.T, i interface{}, fieldNames ...string) {
    t.Helper()

    if reflect.TypeOf(i).Kind() != reflect.Ptr {
        t.Fatalf("given type %T is not a pointer type", i)
    }

    iv := reflect.Indirect(reflect.ValueOf(i)).Interface()
    v := reflect.ValueOf(i)
    tp := reflect.TypeOf(iv)

    if tp.Kind() != reflect.Struct {
        t.Fatalf("given type %T is not a struct type", tp)
    }

    for j := 0; j < tp.NumField(); j++ {
        f := tp.Field(j)
        if !contains(f.Name, fieldNames) {
            continue
        }

        v.Elem().Field(j).Set(reflect.Zero(f.Type))
    }
}
func contains(s string, arr []string) bool {
    for _, ar := range arr {
        if s == ar {
            return true
        }
    }
    return false
}

このignoreField helperは、引数で渡されたstructから、同じく引数で指定されたプロパティ名の値をゼロ値に置き換えます。今回のケースだと、

        ......
        g := goldie.New(t)
        var user UserJSON
        json.NewDecoder(rec.Body).Decode(&user)
        ignoreFields(t, &user, "CreatedAt")
        g.AssertJson(t, t.Name(), user)
}

このように使います。NestedなStructなど、もう少し複雑なケースではまた対応が必要ですが、それに応じたhelperなどを用意しても良いかもしれません。

注意事項

Golden Testとgoldieの使い方を見てきましたが、大変便利である反面、テストとして有効な範囲は限られます。Golden Testで確かめられるのは、以前の結果と変更がないことだけです。 Responseは同じでも、中身のロジックが変わってしまったケースなどはこのテストでは検知できません。

また、出力されたGolden Fileが正しい結果なのかどうかも、テスト自体では確かめることはできません。Golden Fileを出力したら、確実にその結果が正しいのかどうかをチェックするようにしましょう。

加えて、-update を渡すと、全てのGolden Filesが更新されてしまいます。-updateを実行する際には、go testにオプションで実行対象のテストを絞り込み、慎重にupdateを行いましょう。

まとめ

GoのAPI ServerのRegression Testと、それを低コストに始められるGolden Test、そのライブラリであるgoldieについて説明をしました。 Golden Testは簡単に始められますが、実行するたびに値が変わるパターンやGolden Fileの扱いなど、慎重に扱う必要がある場面も多々あります。 使い所は限定されますが、効果的なRegression Testを実現するためにぜひ導入を検討してみてください。

---

1. Snapshot Testingと呼ぶTesting Frameworkもあります↩

2. アラン・ドノバン、ブライアン・カーニハン著　柴田　芳樹訳『プログラミング言語Go』丸善出版株式会社↩

仕様記述テクニック「Promotion」の紹介

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

私はこちらの記事に記載の通り、形式手法の可能性を模索しています。 現在はツールやゲームの仕様を形式的に記述すること（形式仕様記述）で、仕様の欠陥をなるべく早く見つける取り組みにチャレンジしています。 今回は仕様記述をするにあたりよく使う重要な記述テクニックである「Promotion」を紹介します。

形式仕様記述とAlloyというツールを知っている人を対象にしています。 もし形式仕様記述やAlloyをご存じない方は、以前私がbuilderscon tokyo 2019で発表したときに使った資料をご覧ください。

Promotionとは

一般にソフトウェアシステムは複数のコンポーネントから構成されます。 システム全体としての状態（以下、システム状態）は各コンポーネントの状態の組み合わせからなります。 たとえどんなに奥深くのどんなに小さなコンポーネントが変化したとしてもそれはシステム状態の変化になります。

Promotionはコンポーネントの中で起こる局所的な変化をシステムレベルの大局的な変化に"昇格"させるテクニックです。 Promotionはシステム状態の変化といったグローバルな操作を、コンポーネントの変化といった「ローカルな操作」と 「ローカルとグローバルの状態の関係を表す述語」に分解して記述します。

分解せずに記述する方法と比べ、関心の分離ができる上、ローカルとグローバルの状態の関係を表す述語は再利用できるのでリファクタが容易になるといったメリットがあります。

一般的にPromotionは、ローカルの事前・事後を表す変数LocalVariables・LocalVariables'、ローカルの操作を表す述語PredLocal、ローカルとグローバルの状態の関係を表す述語PredPromoteを使い、次の形で表現されます。

これがグローバルな操作と同じ意味になります。

本記事の題材

題材としてGitを扱います。Gitのシステムはいくつかのコンポーネントからなります。 ここでは簡略化してシステムの状態とブランチ、コミット、ファイルの4つの関係を例に挙げます。次の図がその関係の例を示したものです。

ブランチ、コミット、ファイル枠内の丸1つ1つは、それぞれブランチ、コミット、ファイルを表します。
1つのブランチは1つの先頭コミットに紐付きます。あるコミットが、異なる複数のブランチに紐付けられることもありえます。 コミットは0以上のファイルに紐付きます。紐付けられたファイルは、差分ファイルではなくコミットに含まれているファイルを意味しています。
システム枠内の四角1つ1つは、Gitシステムが取りうる「状態」を表します（状態であることを区別するため丸ではなく四角で表現しています）。 状態は「どのブランチ・コミットの関係を持つか」、つまり、存在しているブランチそれぞれがどのコミットを指しているかによって決まります。 1つの状態に対し、「ブランチ・コミットの関係」は1つ以上紐付けられます。

今回はこのシステムを題材に「新しいファイルを追加するコミットを行う」を考えてみたいと思います。

システムの事前状態と事後状態

「新しいファイルを追加するコミットを行う」は、「コミットcに紐付いているある1つのブランチbが別のコミットc'に紐付く（今回はコミットの親子関係を考えない）」という状態変化があります。

図で表すとこのようなイメージです。

事前のシステムの状態をs、事後のシステムの状態をs'と表現しています。 ブランチbはsに紐付けられたブランチです。sでは、ブランチbはコミットcに紐付きます。 「新しいファイルを追加するコミットを行う」を行った結果、s'では、ブランチbはコミットc'に紐付きます。 このとき、c'に紐付けられたファイルは、c'に紐付けられたファイルに新しいファイルを加えたものになります。

共通部分

上の図をAlloyで記述するのに必要な集合、関係は次の通りです。これはPromotionを使う・使わないに関わらず共通です。

sig System {
    bc: Branch -> one Commit
} {
    some bc
}

sig Branch {}

sig Commit {
    files: set File
}

sig File {}

Promotionを使わないストレートな書き方

Promotionを使った書き方を紹介する前にまずは条件をすべてそのまま書き下して書いてみます。

// システムの事前の状態: s
// システムの事後の状態: s'
// 向き先コミットが変わるブランチ: b
// コミットで新しく加わるファイル: newFile
pred commitNewFile(s, s': System, b: Branch, newFile: File) {

      // 【事前条件】追加されるファイルは元のコミットには含まれていない
      newFile not in (b.(s.bc)).files

      // 【事前条件】コミットに含まれるファイルの集合にnewFileを加えたものが新しいコミットのファイルの集合となる
      (b.(s'.bc)).files = (b.(s.bc)).files + newFile

      // s.bcのbの関係を上書き（b以外の関係は変えない）
      s'.bc = s.bc ++ b -> b.(s'.bc)

}

「b以外の関係は変えない」は(Branch - b) <: s'.bc = (Branch - b) <: s.bcとも書けます。

Promotionを使った書き方

先述の通り、Promotionはローカルな操作・ローカルとグローバルの状態の関係を表す述語でグローバルな操作を表現する書き方です。

Promotionを使って書いてみると次のようになります。

// もともと向いていたコミット: c
// 新しい向き先のコミット: c'
// コミットで新しく加わるファイル: newFile
pred commitNewFileLocal(c, c': Commit, newFile: File) {

    // commitNewFile内から必要なものを持ってくる
    newFile not in c.files
    c'.files = c.files + newFile

}

// システムの事前の状態: s
// システムの事後の状態: s'
// もともと向いていたコミット: c
// 新しい向き先のコミット: c'
// 向き先コミットが変わるブランチ: b
pred promoteCommitToSystem(s, s': System, c, c': Commit, b: Branch) {
    
    // 【事前条件】cはbがもともと向いていたcommitであること
    c = b.(s.bc)

    // システムの状態s.bc内のb->cをb->c'で上書き（b->c以外の関係は変えない）
    s'.bc = s.bc ++ b -> c'

}

// システムの事前の状態: s
// システムの事後の状態: s'
// 向き先コミットが変わるブランチ: b
// コミットで新しく加わるファイル: newFile
pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
    some c, c': Commit {
        commitNewFileLocal [c, c', newFile]
        promoteCommitToSystem [s, s', c, c', b]
    }
}

それぞれの述語がどのような役割を担っているのか次の図をもとに説明します。

コミットとファイルに関わるローカルな操作（1の矢印）はcommitNewFileLocal で記述しています。

ローカルとグローバルの状態の関係を表す述語（2-a、2-bの線）はpromoteCommitToSystemで記述しています。 c = b.(s.bc)は、sの中のブランチbに対応するコミットとcが同じであることを意味しています（2-aの線）。 s'.bc = s.bc ++ b -> c'は2つのことを意味しています。1つはs'の中のブランチbに対応するコミットとc'が同じであること（2-bの線）、もう1つはb以外のブランチ（グレーのゾーン）が変化しないということです。 また、promoteCommitToSystemはcがどのように変化するかは関与しません。 そのためpromoteCommitToSystemは他のローカル操作でも再利用ができます。

システムの事前状態sから事後状態s'に関するグローバルな操作（3の矢印）はcommitUsingPromotionで記述しています。 promoteCommitToSystemとcommitNewFileLocalを組み合わせてグローバルな操作を表しています。

同値であることを確認

Promotionを使わない書き方とPromotionを使った書き方は同値なのでしょうか。2つの方法で確かめてみます。

Alloyのアサーションを使って確認

Alloyはアサーション検査ができるのでこの機能を使って確かめてみます。

assert promotion {
    all s, s': System, b: Branch, newFile: File {
        commitNewFile [s, s', b, newFile] <=> commitUsingPromotion [s, s', b, newFile]
    }
}

check promotion

検査をしてみましょう。

Executing "Check promotion"
   Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   1032 vars. 60 primary vars. 2209 clauses. 113ms.
   No counterexample found. Assertion may be valid. 14ms.
   Core contains 4 top-level formulas. 12ms.

結果、反例は見つかりませんでした。 アサーションの検査で可能な有限の範囲に限れば、2つの表現は同値であることが確認できました。

同値変形を使って確認

別のアプローチとして同値変形を利用してみましょう。 まず、commitUsingPromotionの中のcommitNewFileLocalとpromoteCommitToSystemを定義で置き換えてみます。

pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
    some c, c': Commit {
        
        // commitNewFileLocalの定義
        newFile not in c.files
        c'.files = c.files + newFile
        
        // promoteCommitToSystemの定義
        c = b.(s.bc)
        s'.bc = s.bc ++ b -> c'
        
    }
}

限量子someが束縛する変数cはc = b.(s.bc)なので、一点規則と呼ばれる次の規則が適用できます。

すると次のように同値変形できます。

pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
    some c': Commit {
        
        // commitNewFileLocalの定義
        newFile not in (b.(s.bc)).files
        c'.files = (b.(s.bc)).files + newFile

        // promoteCommitToSystemの定義
        s'.bc = s.bc ++ b -> c'
        
    }
}

また先述した通り、s'.bc = s.bc ++ b -> c'には「s'の中のブランチbに対応するコミットとc'が同じであること」という意味があります。 つまり、c' = b.(s'.bc)が成り立ちます。限量子someが束縛する変数c'についても一点規則が適用できます。

pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
    
        // commitNewFileLocalの定義
        newFile not in (b.(s.bc)).files
        (b.(s'.bc).files = (b.(s.bc)).files + newFile

        // promoteCommitToSystemの定義
        s'.bc = s.bc ++ b -> b.(s'.bc)
        
}

本記事で一番最初に紹介したPromotionを使わない書き方commitNewFileと同じ形になりました。

まとめ

Promotionを使えばグローバルな操作をローカルな操作・ローカルとグローバルの状態の関係を表す述語に分けて書くことができます。 操作がローカルな部分のみを変更する場合はPromotionを検討してみると良いかもしれません。

参考

• Using Z

2019年最後のAndroid/iOS Test Nightを開催しました

SWETグループ、iOS自動テスト領域チームの平田（tarappo）とAndroid自動テスト領域チームの田熊（fgfgtkm）、外山（sumio）でお送りします。

おかげさまで、今年でiOS Test Nightは3周年を終えて4年目に、Android Test Nightは2周年を終えて3年目になりました。 皆様のおかげでTest Nightに登録されている資料は156件になりました。ここには素晴らしい知見が集まっています。

そんなTest Nightですが、12/16(月)に2019年最後のTest NightとしてiOSとAndroidを併せておこなったAndroid/iOS Test Nightを開催しました。

今年のTest Nightをすべて振り返りたいところですが、その中でも今年最後のAndroid/iOS Test Nightでの登壇について、SWETメンバーが軽くふりかえってみたいと思います。

Android枠の登壇内容

費用対効果の高いテストコードを書くために考えたこと

• 登壇者：Kaoru Hotateさん

この発表では、テストコードを書く目的の候補4つを挙げ、そこを出発点にテストを書く範囲を決めていく過程が解説されていました。

巷で良く言われている言説をそのまま適用せず、ご自身のプロジェクトの状況と照らし合わせて範囲を絞り込んでいく過程が丁寧に解説されており、とても共感できる内容でした。

絞り込んだ結果はKaoru Hotateさんのプロジェクトにしか当てはまらないとしても、その考え方は他のプロジェクトでも応用できると思います。これからテストを自動化しようと考えている方におすすめの発表でした。

AWS Device FarmとCircleCIでAndroidのUIテストを自動化しよう

• 登壇者：Fumihiko Shiroyamaさん

AWS Device Farmの機能と、Device Farmを活用したテスト実行をCIと統合する方法ついての紹介でした。 また、テストコードなしでデバイス上で自動テストが実行できるFuzzテスト機能のデモを見せていただきました。

Gradleのpluginがあるおかげで導入の敷居は低く、スモークテストをサッとはじめたいときにとてもいいなと思いました。

既存プロジェクトへCI/CDをどう導入するか？

• 登壇者：Horie1024さん

発表の中では、CI/CDの導入をただ単なる技術の導入ではなく、開発チームの文化を変えるきっかけにしている点が印象的でした。

さらに段階的に機能を追加していくうえで、Horie1024さんが実践してきた具体的なプラクティスについても紹介されていました。

SWETチームでもテストやCI/CDの導入を行うことがあるのですが、進め方を考える上で大変勉強になる発表でした。

iOS枠の登壇内容

Xcode 11におけるXCUITestの挙動

• 登壇者：松尾さん

Xcode 11におけるXCUITestの挙動 from Kazuaki Matsuo

Xcode 11ではいろいろな出来事が起きますが、その中でもXCUItestの挙動について話してくれました。

私も出会った事象はありましたが、ここまでいろいろな情報はさすがだなと思います。 Xcodeのメジャーアップデート時などにXCUITestにおいて何かしらの問題に出会ったら、Appiumのissueを見に行くのも１つの方法だと思います。

2019年のSwiftモック事情

• 登壇者：ikesyoさん

Swiftにおけるモック事情について複数のライブラリについて紹介してくれました。

本発表では、最近リリースされたMockoloについても触れていました。 このライブラリはUber製で、コード生成が高速であることがウリになっています。 SWETでも以前調査はしていたのですが、リリースされたばかりの1.1.0については追加調査をしておらず、本発表で改めて試してみないといけないなと思いました。

DeNAからの登壇内容

DeNAからはMOVのiOSアプリ開発をおこなっているsatoshin21とSWETから平田が登壇しました。

GTXiLibで小さく始めるAccessibility Testing

• 登壇者：satoshin21

Accessibilityは重要という認識は広まってきてはいますが、優先順位的に下がりがちではあります。 ただAccessibility Inspectorを使って、常にチェックをするのはなかなか高コストです。 そこで、GTXiLibを使ってテストを小さくはじめようという内容です。

最近、この手の話を聞く機会も増えており重要性がさらに高まってきたと思っています。 私はまだ手を出せていませんが、アクセシビリティについてもテストをしていく必要性を感じています。

iOSにおけるパフォーマンス計測

• 登壇者：平田

iOSにおけるパフォーマンス計測 from Toshiyuki Hirata

Appleはここ数年パフォーマンスに関する機能を提供してきています。 また、パフォーマンス改善に関するドキュメントなども提供しています。

iOSにおいてはどのように改善サイクルを回すと良いのか、またその時に利用できるもgのとして何があるのかについて登壇をしました。

最近、パフォーマンス周りについて力を入れていることもあり今回のような登壇をしました。 お話しきれなかったことも多くありましたので、また何かしらの形でアウトプット出来ればと思います。

ブログ枠のまとめ

ウホーイさんが作成してくれました。 各発表のTwitterでの反応がまとまっており、当日の盛り上がりが伝わってきます。 いつもありがとうございます。

Test Nightのまとめです！
2019年ありがとうございました✨#test_night
---
I just published 【勉強会】「年末だよ Android/iOS Test Night — 2019」まとめ https://t.co/U7b8vUB9UC

— ウホーイ (@the_uhooi) December 17, 2019

最後に

2019年、皆様のおかげで素晴らしいTest Nightを合計9回も開催することができました。 2020年もTest Nightなどを通してさらなるナレッジを皆様と一緒に世に届けられたらと思います。

最後の最後に、 SWETの仕事に興味を持った方は、SWETメンバーに声をかけていただければと思います。

モブプログラミングワークショップを開催した話

この記事は、モブプログラミング Advent Calendar 2019の20日目の記事です。

SWETグループの長谷川（@nowsprinting）です。

先日、AGILE MONSTERの及部さん（@TAKAKING22）をファシリテーターにお招きし、SWETでモブプログラミング（以下モブプロ）のワークショップを開催しました。

SWETの取り組みの中には、DeNA内の多様なプロダクト開発チームに対してテスト技術を伝える・サポートすることも含まれています。 その活動においてモブプロは有効な手段ではないかと考え、より効果的なセッションを運用するためのノウハウを得たいというのが目的です。

この記事では、ワークショップを通して感じたことなどをまとめて紹介します。

ワークショップ

ワークショップ内容は、及部さんの『Head First モブプログラミング』をカスタマイズした資料でのイントロダクション、モブセッション、発表会、振り返り、『小さなチーム、大きな仕事を実装するモブプログラミング』＋αの講義、という構成でした。

＋αの部分では、我々SWETが今後モブセッションをファシリテートしていくための知見を話していただけるようリクエストしていましたが、そのアンサーは

• ファシリテートしない
• カオスを受け入れる

の2点でした。 言葉だけ見ると突き放すようなインパクトがありますが、実際にワークショップを通して聞くと納得感を得られるものでした。

この2点のアンサーを含め、ワークショップ開催にあたって及部さんが整理されたであろう内容がアドベントカレンダー1日目の記事『モブプログラミングを導入するときに考えていること』に書かれていますので、ご興味ある方はあわせて参照をおすすめします。

モブセッション

モブセッションでは、3〜4人ごとのチーム（モブ）に別れ、それぞれ1台のPCで「自動販売機の機能を実装する」という課題に取り組みました。

以下、私のいたモブの話をします。

課題の「自動販売機」に対し、MVP（Minimum Viable Product）だけ定義してあとはTDD（Test Driven Development：テスト駆動開発）でやりましょう！　と、一番早くホワイトボードから離れ作業に入りました。 しかし進めるうち、ストーリーでなく機能に目が行ってしまったり（例えば「品切れ」などの考慮をしはじめたり）、コレクションをどこに持つかのコンセンサスが取れていなくてホワイトボードに戻ったりと迷走し、最初のテストが通ったところで前半セッションを終了。

休憩後の後半から、ようやくTDDが回りだしたものの、最後にテストを壊したところでタイムアップ。成果物としては悔いの残る結果に終わりました。

タイピスト（ドライバー）交代にはMobsterを使いましたが、要所要所でコミットをちゃんと残すことに意識が行かず（結局はじめにgit initしただけでノーコミット）、実際の業務でモブプロする場合には別の交代契機を検討したほうが良さそうという学びを得ました。

個人の感想とまとめ

これまでは、モブプロの業務効率についてはあまり意識していませんでした。 しかしワークショップを通じて、通常の分担作業前後のミーティングがモブプロに包括される効果やフロー効率の良さを感じられ、普段からモブプロで業務を進めるという選択も現実的ではないかと思うようになりました。

特に、SWETとしては普段から自動テストの効用として、不具合を早期に発見にすることの価値を伝えていますが、モブプロによる細かい軌道修正は同様の効果がありそうです。

ほかに印象に残ったのは、同じSWETとはいえ普段同じプロジェクトで仕事をしているわけではないので、お互いのテストの書き方の違いを見られる・教え合えるのは新鮮で楽しい体験でした。 Pull Requestレビューでは経緯や細かい点までわざわざ書かないものなので、ペアプロ/モブプロをしないとわからなかったことでしょう。

今後の取り組み

テストなどのノウハウの共有を目的とするモブプロは、ペアプロに誘うより心理的障壁も低く、セッション中の負荷も軽いため、積極的に使っていこうと試行をはじめています。 そのために、（普段のチーム開発ではなく）アドホックに実施するモブプロに最適なテンプレート的なものの整備も進めています。

またモブプロでは、エンジニア経験が少ない人や他の職種の人であっても、まわりがナビゲートすることでタイピストが務まります。

ゲーム開発ではエンジニア以外の様々なロール¹と連携して開発を進めていきますが、ところどころでモブプロに参加してもらうことでお互いの考えを知り、暗黙知を共有できるのではないかと考えています。 当初想定していた「テスト技術を伝える」ためだけではなく、モブプロそのものの良さを伝え、社内各所で試してもらえるように活動していきたいです。

以上のような試みに共感していただけた方、興味を持たれた方、一緒に働いてみようと思ってくれた方。 下記職種で採用しておりますので、ぜひご応募ください。お待ちしております。

テスト自動化エンジニア（Unity Test）

テストエンジニア （ゲームアーキテクチャ）

また、その他の分野へのご応募もお待ちしております。 募集職種に関してましては、本ブログサイドバーの「採用情報」の項目をご覧ください。

---

1. プロデューサー、ディレクター、プランナー、サウンドディレクター、UIデザイナー、エフェクトデザイナー、グラフィックスプログラマー、QAなど↩

SWETの2名が執筆に加わった「iOSテスト全書」が一般発売されました

SWETグループ、iOS自動テスト領域チームの平田（tarappo）です。

長いことおまたせしましたが、12/16（月）に「iOSテスト全書」が一般発売されました。 私と同じくSWETの細沼（tobi462）が執筆に加わっています。

※12/16(月)に開催されたiOS / Android Test Nightの開始前に写真を撮りました。

本書の一般販売を記念して、本エントリーでは本書全体の概要と見どころについて解説します。 また、併せてすでに発売済みの「iOSアプリ開発自動テストの教科書（以後、教科書本）」との想定読者の違いについても説明します。

本書の企画

本書の企画は、私が相談をして進めさせてもらいました。

昨年（2018年）「Androidテスト全書」の執筆に関わり、周りからの意見もありiOSアプリ開発においても、このようなテストについての本の必要性を強く感じていました。

iOSアプリ開発においては、テスト周りにおいて体系的にまとまった情報はあまりありません。 一歩踏み込んだ情報となると、日本語でのネット情報は少なくその情報自体最新のものなのかわからないといった状況でもありました。

「iOSテスト全書」の企画を立ち上げる前から、私と細沼は「教科書本」の執筆について話が進んでおり執筆がスタートしはじめていました。 この本はその名の通り教科書として最初の一歩として道標になると思ってはいたものの、この本だけでは不足している面もあるだろうとも思っていました。

そこで、「iOSテスト全書」としてさらに一歩の情報まで載せた本を世に出したいと思い、執筆に加わってほしい人たちに声をかけました。

Androidテスト全書が一般発売されたのは2018年11月5日になります。 そこから2週間後、11月19日が執筆者と編集者が揃った「iOSテスト全書」のキックオフの日になります。 そして2019年1月28日にクラウドファンディングがスタートし、このたび一般販売となりました。

思っていたよりも時間がかかってしまいましたが、良いものができたと思います。 ぜひ、手にとっていただければと思います。

本書の概要

本書の目次は次のとおりです。

• 1章：テスト自動化入門
• 2章：ユニットテスト（概要）
• 3章：ユニットテスト（XCTest編）
• 4章：ユニットテスト（Quick／Nimble編）
• 5章：BDDによるアプリ開発
• 6章：UIテスト入門
• 7章：XCUITestを使ったUIテスト
• 8章：サードパーティ製ツールとAppium
• 9章：CI／CD

自動テストに対する話から、ユニットテスト・UIテスト、そしてそれらを実行するCI／CDについてまで触れています。 この中から細沼が2章〜5章（3章共著）、平田が6章と9章を担当しています。

「教科書本」はテストに関するものを幅広く扱い、その名前の通り教科書として最初に活用してもらうことを想定しています。 「iOSテスト全書」では、より一歩進んだところにもいけるよう自動テストやCI／CDについてもう少しふみこんで書いてあります。

このようなiOSアプリ開発におけるテスト周りにフォーカスした本が2019年に2冊も出たということは凄いことだと思っています。 是非ともiOSアプリ開発をおこなっている方は、本書を手にとって頂いて書いてある内容にチャレンジしてみてください。

本書の想定読者

本書の想定読者はPEAKSのページに書いてあるとおり次の方になります。

• テストについて興味はあるがどうしたらいいかわからない方
• テストについてもっとよい書き方があるのではないかと悩んでいる方
• テストにもっと強くなりたい方
• CI/CDサービスをもっと活用したいと思っている方

iOSアプリ開発に携わる人であれば、なにかしら得られるものがある内容になっています。

各章の見どころについてはそれぞれの執筆者が書いてくださると思っています。 ここでは、我々が執筆した章についての見どころについて次に説明していきたいと思います。

2章〜5章の見どころ（細沼担当）

個人ブログ記事でも書かせていただきましたが、 私が担当した2章、4章、5章はそれぞれ明確なコンセプトをもって執筆をさせていただきました。

2章は『iOSに限定されないユニットテストの知識』をテーマにして、 ユニットテストにおいて一般的に利用できるテクニックを紹介しています。

個人的な見どころは『テストコードの保守性を上げる』のトピックです。 XCTestを使った愚直なテストコードの例からはじめ、 テストコードを徐々にリファクタリングしながら保守性を上げる過程がわかるようになっています。

3章は共著として一部のみを担当しました。 具体的には『テスト実行の単位を管理する方法』として、 これまで利用されてきた『スキーム』を使った方法に加え、 Xcode 11から追加された『テストプラン』の利用方法について記載しています。

このあたりは中々分かりづらい機能ですが、 個人的にわかりやすく解説できているのではと感じます。

4章は『日本語における最強のQuick／Nimbleリソース』をテーマとして執筆しました。

Quick／Nimbleは公式でもドキュメントが整備されているOSSですが、 知識を体系的に積んで学ぶという点においては、個人的に不足を感じていました。

そこで知識を一から積んでいけるように構成を工夫し、 分かりづらい機能についても、できるだけ丁寧な解説を心がけています。

5章は『私が今まで得てきた知恵や経験を、書籍を通して読者に』をテーマにし、 Quick／NimbleとBDD（振舞駆動開発）を利用してサンプルアプリを開発する内容になっています。

2章〜4章で解説してきた静的なテクニックをつなぎ合わせ、 動的なストーリーとして理解を深められる構成になっています。 そういった意味で、2章〜4章で学んできた内容を締めくくる、ユニットテストにおけるまとめ的な章になっています。

6章、9章の見どころ（平田担当）

6章の「UIテスト入門」については、UIテストをおこなっていく上で、次のようなフェーズ単位で気にすべきことをまとめました。

• 導入前に検討したほうがいいこと
• 実装中に考慮すべきこと
• 運用時に注意するべきこと

UIテストは実装して、動いているのを見ると「なんか凄い！」と実装者自身やチームメンバーが感じやすいです。 その結果、闇雲にテストコードを追加し、その結果として負債となるコードが生まれることもあります。

一旦落ち着いて何をするべきかを考えることが重要です。 そこで筆者の経験などを元に、UIテストが実際に現場で活用できるように、それぞれのフェーズで気にすべきことをある程度まとめました。

9章の「CI／CD」では、「CI／CDとはなにか」について厚めに述べています。 本来は、この話だけで1冊になってしまうぐらいの話ですが、次のようなトピックに注力し説明をしています。

• CIとはなにか？
• CDとはなにか？
• どのようなワークフローを組むか

このような内容は、特定のサービスに限らず他でも汎用的に利用できるものです。

しかし、実際に利用した形も見ないとイメージが分かりづらいのも事実です。 そこで、述べたワークフローの例をもとにiOSアプリ開発で人気のCI／CDサービスであるBitriseを用いて説明をしています。

本章の内容により、自社のプロダクトにおいてどのようなワークフローを用意するのが良いかを考える一助になってくれると筆者としては嬉しい限りです。

おわりに

今回は、一般発売がはじまった「iOSテスト全書」について解説させていただきました。 この本が何かしら皆さんにとってプラスとなり、そして今後テストに関する情報がいろいろな媒体を通して世に出てもらえれば筆者としては嬉しい限りです。

また、我々SWETとしては今後「教科書本」や「iOSテスト全書」を社内で活用するよういろいろとおこなっていく予定です。 まだ何かしら具体的な活動はそこまで行えておらず、世へのアウトプット出来ていませんが、今後のアウトプットをお待ちいただければと思います。

そして、これらの活動に興味がある方はぜひとも次から書かれている内容を元に仲間となっていただけると嬉しい限りです。

仲間を募集中

SWETチームでは自動テストやCI／CDを活用する仕事に興味を持った方を募集しています。

以下のエントリフォームから応募できるほか、 私や他のSWETメンバーに声をかけて頂くかたちでも大丈夫です。

是非ともお気軽にご連絡ください！

• テスト自動化エンジニア（iOS Test）
• CI/CD基盤エンジニア