DeNA Testing Blog

Make Testing Fun, Smart, and Delighting End-Users

形式手法でデータ構造を記述・検査してみよう:Alloy編

SWETの仕様分析サポートチーム所属のtakasek(@takasek)です。

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

当記事は、Kuniwak(@orga_chem)により社内開催されたAlloyガイダンスを元に再構成した記事です。よく知られたデータ構造であるStackを形式仕様記述しビジュアライズすることで、Alloyの使い方と利点を実感できます。Alloy未経験者でもステップバイステップで試せるように構成しました。是非、お手元にAlloyをインストールして読み進めてください。環境はAlloy 5.1.0を想定しています。

https://github.com/AlloyTools/org.alloytools.alloy/releases

Alloyとは

形式手法の言語およびツールです。システムの構造の制約や振る舞いを簡易に、しかし強力に記述できるようデザインされています。記述されたモデルは要素同士の関係グラフとして視覚化できるというのが特徴です。

もっとも単純なモデルを記述する

Alloyのエディタを起動したら、以下を記述してください。

sig A {}

f:id:swet-blog:20200501184146p:plain

sig はsignatureを意味し、atom(要素)の集合を示します。signatureはオブジェクト指向プログラミングのclassと書き方がなんとなく似ていますが、その実態はまったく異なるものなのでご注意ください。

Executeの結果

ExecuteボタンをクリックするとVisualizerが開きます。Visualizerでは、Nextボタンをクリックするたびにインスタンスが次々とグラフとして表示されます。インスタンスというのは、関係における変数を特定の値で束縛したものです。1

f:id:swet-blog:20200501184029g:plain

Aのatomが0, 1, 2, 3, 4個存在する例を確認できました。現実的には当然5個以上になることもありますが、個数が増えると探索コストが急激に増大するためAlloyは割り切ってデフォルトの探索範囲を少なくしています。それでもおおよその反例は見つかるだろうという前提を小スコープ仮説といいます2。もし無限のケースについて正しさを証明したい場合は、CoqやIsabelleに代表される定理証明支援系の技術が必要になります。

2シグネチャの関係を記述する

sigを2つに増やして、その関係を記述してみましょう。

sig A {
    b: B // 集合Aに属する各々のatomは、集合Bに属するただ1個のatomと関係を持つ
}

sig B {}

Executeの結果

抜粋すると…

関係 グラフ
Aの要素:0個
Bの要素:1個
Aの要素:1個
Bの要素:2個
Aの要素:2個
Bの要素:2個
Aの要素:2個
Bの要素:2個

最後の例があることは提示されて初めて気づく人も多いのではないでしょうか。このように、パターンを網羅的に目で見て確認できるのがAlloyの良いところです。

関係の多重度は、さまざまな形で表現可能です。

sig A {
    b: B, // 1個の要素への関係
    c: one C, // 1個の要素への関係(※省略はoneを意味する)
    d: lone D, // 0〜1個の要素への関係
    e: set E // 0個以上の要素への関係
    // 他にもあります
}

Stackを表現する

ここからが本題です。Stackをモデルとして記述していきましょう。見慣れた連結リストです。

sig Stack {
    value: univ,
    next: lone Stack
}

Stack というsignature、すなわち集合を定義しました。

Stackvaluenext という2つのフィールドを持つsignatureです。フィールド value は、Stackに属する各々のatomと、univに属するただ1個のatomとの関係を示します。フィールド next は、Stackに属する各々のatomと、Stackに属する0〜1個のatomとの関係を示します。なお、univは「あらゆるatomが属する集合」を意味しています。

(勘の良い方は、このモデリングに「おや?」と思われたかもしれません。後ほどその点にも触れますので、今はこのまま読み進めてください)

ここまで書けたら、Executeします。

ビジュアライズの結果を読み解く

結果を見る前に…

f:id:swet-blog:20200501184118g:plain

数値が変わるだけの同じような例が連続して出てきてキツいですね。よく見るとVisualizerのステータスバーに Run Default for 4 but 4 int, 4 seq expect 1 とあります。実はAlloyは、Executeの対象がない場合は暗黙的に以下のような出力命令が省略されているものと解釈しているようです(Alloy5現在)。

run{} for 4 but 4 int, 4 seq expect 1

for 以下は、Visualizerの表示要素数の範囲(スコープ)を示します。なお省略されたrunに任せず明示的に run {} と書いた場合には、 run{} for 4 but 4 int, 4 seq expect 1 よりも少量のインスタンスがビジュアライズされるようです。なぜそうなるのかは調査できていません。

ビジュアライズ結果を読み解く

run {} で再度Executeして、ビジュアライズされた関係グラフを読み解きましょう。最初のグラフはこれですが…

いきなり想定外のグラフです。Visualizer上の Stack のnextが自分自身になっています。データ構造としてStackは循環を許しません。

「Stackは循環しない」という不変条件を書く

Stackが循環しないことを示すためには「このモデルは常にこうなる」という制約を与える論理式(不変条件)を書く必要があります。sig 内の記述だけに着目すれば成立するインスタンスでも、与えられた制約に違反する場合はビジュアライズされません。

「nextは自分自身にはならない」ことを示す

ただし不変条件を正しく書けなかった場合、正常なはずのインスタンスも表示されなくなってしまい、かつそれに気づけないリスクがあります。人間は異常なものを見つけることは得意ですが、あるべき正常なものの欠損に気づくのは苦手です。まずは論理式が本当に過不足のない制約を表現しているかを確認すべきです。

そのために表明(assert)を使います。不変条件はモデルに対して強制的に適用される論理式ですが、表明は現状のモデル自体には影響を与えず「モデルの制約はそうなっているはず」を表現する論理式です。3

今回、Stackが循環しないことを示すには「nextは自分自身にはならない」論理式を書きます。

// 「すべてのStackについて、自身のnextの集合に、自身が含まれない」という表明
assert TestRecursion {
    all s: Stack | s not in s.next
}
// check命令は、表明に違反するインスタンスがないかを確認します
check TestRecursion

ツールバーから Execute > Check TestRecursion すると、コンソールに以下のようなメッセージが表示されました。

Executing "Check TestRecursion"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   483 vars. 72 primary vars. 827 clauses. 7ms.
   Counterexample found. Assertion is invalid. 3ms.

反例(counterexample)、すなわち現状のモデルの中で表明に違反するインスタンスが見つかりました。グラフとして確認できるので見てみましょう。

いいですね。「すべてのStackについて、自身のnextの集合に、自身が含まれない」の反例……すなわち「自分自身がnextになる」インスタンスだけが出力されています。表明をそのまま不変条件に昇格させれば「常にモデルがそれを満たす」という制約の記述になります。

記述全体は以下のようになります。不変条件の記述は fact です。

sig Stack {
    value: univ,
    next: lone Stack
}
fact NoRecursion {
    all s: Stack | s not in s.next
}

不変条件を加えたモデルが想定どおりか、runして確認していきましょう。

run {}

すると、気になるものが見つかりました。

あるStack自身の循環はなくなりましたが、 Stack0.nextStack1Stack1.nextStack0 という間接的な循環が残っています。

「nextを辿った先が自分自身にはならない」ことを示す

「nextは自分自身にはならない(s -(next)-> s)」ことは示しましたが、それだけでは足りなかったのです。 s -(next)-> ... -(next)-> s という関係を表現する必要があります。

そのためには推移閉包を使います。厳密な定義は置いといて、ざっくり言えば「関係Rについて s1 -(R)-> s2 s2 -(R)-> s3 が言えるとき s1 -(R)-> s3 も言える」という関係の集合が推移閉包です。Googleイメージ検索したら感覚は掴めると思います。Alloyには推移閉包オペレータがあり、 ^ をつけるだけで推移的関係を表現可能です。

……というのは本当でしょうか? 我々には確認の手段があります。Alloyの力を借りましょう。 fact NoRecursion はそのまま、表明を追加します。最初に書いたTestRecursionからの差分は、nextに推移閉包オペレータをつけただけです。

...
fact NoRecursion {
    all s: Stack | s not in s.next
}
assert TestRecursion {
    all s: Stack | s not in s.(^next)
}
// 似たようなIntの例が多すぎて邪魔なので、forでスコープを絞ってcheckします
check TestRecursion for 2 Int

再びツールバーから Execute > Check TestRecursion します。さっき見つけた双方向の矢印のパターンが反例として上がってくればしめしめです。どうでしょうか……

nextが双方向の矢印になる例だけが見つかりました。Stackの表示要素数が2個より多い場合の関係も検査してみましょう。

check TestRecursion for 2 Int, 4 Stack

3個のStackが循環参照している反例が見つかりました。いい感じです。

では、表明を不変条件に格上げします。

fact NoRecursion {
-    all s: Stack | s not in s.next
+    all s: Stack | s not in s.(^next)
}

含意の確認をする

ちょっと待ってください。本当にこの格上げは正しいのでしょうか。推移閉包によって「nextを辿った先が自分自身にはならない」ことを表現できました。しかし、これを満たすとき、今までの「nextは自分自身にはならない」も満たすかと言われると確証がありません。感覚的には間違っていないように思えますが、論理の力で保証したいところです。

つまり、論理式「『nextを辿った先が自分自身にはならない』ならば『nextは自分自身にはならない』」が正しいことを確認したいのです。

assert TestImplies {
    (all s: Stack | s not in s.(^next))
        implies (all s: Stack | s not in s.next)
}

implies は含意、つまり論理学の初歩で習う「AならばB」です。

check TestImplies をExecuteすると、コンソールに以下のメッセージが表示されました。

Executing "Check TestImplies"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   560 vars. 72 primary vars. 907 clauses. 16ms.
   No counterexample found. Assertion may be valid. 2ms.

反例が見つからないということは、「『nextを辿った先が自分自身にはならない』ならば『nextは自分自身にはならない』」は正しいようです。不変条件の格上げは適切だと自信を持てました。

valueの不変条件を書く

ここまでで、全体の記述は以下のようになっています。

sig Stack {
    value: univ,
    next: lone Stack
}
fact NoRecursion {
    all s: Stack | s not in s.(^next)
}

run {} for 1 Int

runの結果……

value周りにおかしな関係が見つかりました。「Stack0.nextStack1」「Stack1.nextStack1」など、あるStackのvalueがStackだったケースでは循環が生まれてしまうようです。

その原因は、valueの属する集合が univ すなわち「あらゆるatomの集合」になっているせいです。

どのように対処しましょうか。

  • valueフィールドとnextフィールドの関係を適切に記述する
  • 「valueはStackにならない」という仕様で逃げる

理想的なのは前者ですが割愛します。腕に自信のある方は正面突破してみましょう。今回は「valueはStackにならない」という仕様を導入して逃げることにします。より厳密な日本語で表現するなら「すべてのStackについて、自身と関係するvalueはStackではない」というべきでしょうか。

assert TestValue {
    // ここに「すべてのStackについて、自身と関係するvalueはStackではない」という論理式を書く
}

もしあなたが手元にAlloyをインストールして進めているなら、ちょうどいい練習問題なので自分で書いてみましょうか。すこしスペースを空けますね。

...

...

...

...

...

答え合わせです。 答えのひとつは、次のとおりです。

assert TestValue {
    all s1, s2: Stack | s1.value not in s2
}

check TestValue for 1 Int, 4 Stack で検査してみるといいでしょう。

論理式をリファクタする

実は all s1, s2: Stack | s1.value not in s2 はベストな解ではありません。よりシンプルに書くなら、

all s: Stack | s.value not in Stack

で十分です。

そういうことなら…と書き換える前に、一度立ち止まりましょう。プログラミングでもそうですが、リファクタリングでは修正前後に記述の意味が変化してしまってはいけません。論理の世界の言葉で言い換えると「修正前の論理式と修正後の論理式が同値である」ことを確かめたいです。

そこで、式変形前後での同値性の確認のテクニックを紹介します。手順は先述した含意の確認とよく似ています。

assert TestTrans {
    (all s1, s2: Stack | s1.value not in s2)
        iff (all s: Stack | s.value not in Stack)
}

iffif and only if の略で「Bのときに限りAが成り立つ。Aが成り立つのはそのときに限る」つまり必要十分条件を示します。そのような論理式は同値として扱えます。オペレータとして <=> と書くこともできます。

check TestTrans をExecuteすると、コンソールに以下のメッセージが表示されました。

Executing "Check TestTrans"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   1158 vars. 69 primary vars. 2196 clauses. 7ms.
   No counterexample found. Assertion may be valid. 3ms.

反例が見つからないということは、修正前後の論理式は同値だということです。より大きなスコープで反例が見つかる可能性を頭の片隅に常に置いておく必要がありますが、今回は大丈夫でしょう。自信を持って書き換えましょう。なお、もし反例があった場合にはVisualizerでグラフとして確認可能です。Alloyは便利ですね。

完成したモデルを確認

sig Stack {
    value: univ,
    next: lone Stack
}
fact NoRecursion {
    all s: Stack | s not in s.(^next)
}
fact NoRecursiveValue {
    all s: Stack | s.value not in Stack
}

この記述が適切なものか確認しましょう。

run {} for 1 Int, 4 Stack

よさそうです。

push, popの前後関係をpredで表現する

データ構造のStackに対しては、pushとpopという操作が可能です。その確認もしたいです。

Alloyの状態モデルではミュータブルな手続きを書くことはできません。かわりに操作前後の状態を別物(事前状態、事後状態)として扱います。事後状態は慣習的に ' をつけて表記します。

  • push前のStack = s
  • push後のStack = s' (読みはs-prime)

s になんらかの値をpushした状態」と「s'」が同値だと示す論理式を書けば、前後の関係が表現できます。

任意個数の変数から真理値(true/false)を導く論理式を述語(predicate)といいます。これまで書いてきた run {}{} も、実は述語です。このrun命令は、次のように分解できます。

pred P {} // 述語の宣言と定義
run P     // 定義した述語に対する出力命令

pushを表現したいなら、次のような三変数述語になります。なお改行はandを示します。

pred Push[s, s': Stack, x: univ] {
    s'.value = x
    s'.next = s
}

この述語を満たす関係を run Push for 1 Int, 4 Stack でビジュアライズすれば、push前後のStackの関係が読み取れます。

上図の表記は、以下を意味します。

  • $Push_sPush の変数の s
  • $Push_s'Push の変数の s'
  • $Push_xPush の変数の x

sx をpushした結果が s' になることが図示できていますね。

popについても同じように書けます。難しいところはないので特に説明しません。練習問題として試してみるとよいでしょう。

まとめ

AlloyでStackを記述・検査する一連の流れを通じて、Alloyの使い方を紹介しました。とっつきやすいツールですので、是非ご活用ください。

仕様が妥当なものか確認せずに、手続き的に複雑な仕様を作り上げてしまうことはよくあります。形式仕様記述を用いて仕様をシンプルに書き、ときにリファクタしながら研ぎ澄ませると、より安全で自信に満ちあふれた開発プロセスが手に入るかもしれません。

なお、本記事よりも高度な記述が知りたい場合は公式のlanguage referenceをご参照ください。 https://alloytools.org/download/alloy-language-reference.pdf

SWET視点でピックアップしたテストに関するWWDC 2020まとめ

お久しぶりです。 SWETグループの平田(@tarappo)と片山(@kariad_uu)です。

本稿では、先日オンラインでおこなわれたWWDC2020の中から、SWET視点で気になった次の2点について紹介したいと思います。

  • The suite life of testing
  • Instruments周り

これら以外にもテスト周りの追加としては待望の「Xcodeを用いたStoreKitのテスト」がありますが、本記事では割愛します。

本記事でアップしているXcodeの画像はXcode11.6でとった画像となります。 Xcode12では見た目が変わっている可能性があります。

The suite life of testing

まず、WWDC2020で公開された「The suite life of testing」について平田が紹介していきます。

WWDC2020では「The suite life of testing」として次の5つの動画が公開されています。

  • Handle interruptions and alerts in UI tests
  • Get your test results faster
  • XCTSkip your tests
  • Triage test failures with XCTIssue
  • Write tests to fail

これらの動画での説明はそれぞれがある程度関係をしていて、大きくまとめると「自動テストが失敗したときの対応」についての話がメインといえます。

そこで、ここでは1つ1つの動画の中身について説明するのではなく、これらの動画を簡潔にまとめて説明をします。 (なお「Handle interruptions and alerts in UI tests」についてはUIテスト時の割り込みやアラートをどのように対応するかの話なので今回は除外します)

自動テストは常に成功するわけでなく失敗もします。 この自動テストの失敗時の調査は、テストコードを維持し続けるために大事なことです。 しかし、調査にコストがかかりすぎてしまうのは問題です。

このコストがかかりすぎないように、動画内でも説明されているものとして、次の2つの観点で説明をしていきます。

  • フィードバックを早くする
  • フィードバックからの情報取得

フィードバックを早くする

自動テストからのフィードバックは早いことが望ましいです。 たとえば、CI/CDサービスで自動テストを動かしていて、いつまでたっても終わらないといったことが起きてしまうと結果を待ちきれなくなってしまいます。

その結果、自動テストを実行しないといったことにもつながってしまう恐れがあります。

次をおこなうことでフィードバックを早くできます。

  • テストの実行時間の制御
  • テストのスキップ
  • 並列実行

これらについて次に説明をしていきます。

テストの実行時間の制御

必要な理由

テストの実行時間がのびてしまう原因の1つとして、自動テストが想定の時間以上かかってしまうということがあります。

たとえば、テストのハングにより自動テストが終わらなかったとします。

その場合、CI/CDサービスの制限時間や実行している環境(デバイスファームなど)の制限時間により、テストが無理やり終了させられてしまうことになります。

そうすると、テストが無事に終了していないため自動テストの結果を得ることも出来ずに、なにが問題だったのかがわからなくなってしまいます。

Xcode11.4でテストの実行時間を制御できるようになりました。

この機能を利用することで、特定の時間以上がかかった場合にそのテストを失敗扱いにできます。

これにより、想定外の挙動をしてテストが終了せずに実行時間が長くなってしまうといったことを止めることができます。

制限時間の設定

本機能はTestPlansで下記画像にあるように「Test Timeouts」をONにすることで利用できるようになります。

f:id:swet-blog:20200813095532p:plain

テストの制限時間はデフォルトで10分が指定されています。 この値は、複数の方法で変更できます。

その際の優先度は次のとおりです。

  1. テストコード側で利用するexecutionTimeAllowance API
  2. テスト実行時に指定するxcodebuildのtimeallowanceオプション
  3. TestPlansの設定
  4. デフォルトの時間(10分)

これらの設定方法のうち、Xcode12から3にあるTestPlansからも値を設定できるようになりました。

これらの指定する値は、秒数で指定できますが注意が必要です。 たとえば、60秒未満を指定した場合は1分に切り上げられます。 100秒であれば、2分に切り上げられます。

この指定した時間以上に実行時間がかかった場合、Xcode上では次のようなエラーが表示されます。

f:id:swet-blog:20200813095427p:plain

この画像の例では制限時間を1分と指定していて、テストの実行時間がその時間を過ぎています。

なお、エラーが出たときの情報の詳細はXcode12からより詳細に出るようになったので、後述します。

テストのスキップ

必要な理由

自動テストを実装している中で、実行する環境に依存するようなテストを実装することもあります。

たとえば、ユニバーサルアプリでiPadのみで動くテストとか、特定のOSバージョン以上で動作するテストなどです。

これらはすべてテストの実行時にしか判断できない条件になります。 今まではXCTestではテストの結果は「成功」または「失敗」しかありませんでした。

そのため、実行環境によって動かないテストは求めている実行環境以外で動作したときに「成功」または「失敗」のどちらかになるようにするか、またはそのテスト自体を無効化するかといった選択肢しかありませんでした。

成功とすると、テストを実行していないのに問題ないという判定をすることになります。 失敗とすると、何も問題が発生していないのに落ちた原因をチェックするコストを使うことになります。

Xcode11.4からテストをスキップできるXCTSkipというAPIが追加されました。 これにより、特定の条件の際に自動テストをスキップできます。

XCTSkipを利用してテストのスキップ

このXCTSkipを利用することで、明示的にテストを特定条件の際にスキップできます。

例えば次のコード例のようにXCTSkipUnlessを利用することで、実行デバイスがiPadでなければテストをスキップできます。

func testSkipExample() throws {
    try XCTSkipUnless(UIDevice.current.userInterfaceIdiom == .pad, "iPad only")
    
    //なにかしらの処理
}

このようにテストをスキップさせた場合、Xcode上では次のように表示されます。 今までは「成功の緑」と「失敗の赤」だけでしたが、この「スキップのグレイ」が増えました。

f:id:swet-blog:20200813095549p:plain

また自動テストはCI/CDサービスで動かすと思います。 そのため、CLI上で動かしたときに生成されるテスト結果にもテストが成功・失敗の情報だけでなくスキップされた情報も必要になります。

利用できるテスト成果物として、Xcode11から追加されたResult Bundleがあります。 このResult Bundleは次のコマンドを用いることでJSONフォーマットとして情報を生成できます。

$ xcrun xcresulttool get \
  --path ResultBundle.xcresult \
  --format json

生成された情報の一部は次のようになります。 これを見るとわかりますが、testSkippedCount としてスキップの情報もあることがわかります。

  "metrics" : {
    "_type" : {
      "_name" : "ResultMetrics"
    },
    "errorCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "2"
    },
    "testsCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "3"
    },
    "testsFailedCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "1"
    },
    "testsSkippedCount" : {
      "_type" : {
        "_name" : "Int"
      },
      "_value" : "1"
    }
  }

このResult Bundleを活用することにより、CI/CDサービスで自動テストを実行した場合でも、テストの「成功」「失敗」「スキップ」といった情報を取得できます。

Result Bundleについては、以前本ブログで書いた記事を参考にしてもらえればと思います。

並列実行

必要な理由

並列実行は自動テストにおいてよくある実行時間の短縮の方法です。 テストを分割しておこなえるために、トータルとしての実行時間が短くできます。

XCTestにおいてもいろいろな方法で並列実行をおこなうことができますが、Xcode10からiOSシミュレーターの並列実行が容易にできるようになっています。

ただし、並列実行をすれば必ずしも実行時間が確実に短縮されるわけではありません。 ある特定のテストケースだけ実行時間が長いと、トータルの実行時間はそのテストケースに引っ張られてしまいます。

このXcode10から追加された並列実行の方法や注意点については、以前書いたSWETブログの記事を参考にしてください。

Xcode12における並列実行

Xcode11.4からxcodebuildコマンドを利用すると、iOS/tvOSの実機に対して並列実行を行うことができるようになりました。

これにより、iOSシミュレーター / iOS実機と並列実行をできるようになり、いろいろなパターンで自動テストを実行できるようになりました。

本機能による並列実行の注意点として、自動テストがどの端末に割り当てられるかは指定できません。 (XCTestでは実行するテスト/実行しないテストを指定できるので、どの端末にどのテストを指定するかを決めることによる並列実行もできますが、手動管理になるため大変です)

そのため、基本的には同一のデバイス・同一のOSバージョンで端末を用意しておくのが理想的です。

同じ端末を用意できずに、異なるデバイスやOSを使って自動テストの並列実行する場合は、デバイスやOSに依存するようなテストは実行しないのが望ましいです。

フィードバックからの情報取得

テストが常に成功するのであれば、テストからのフィードバックに付加的な情報はそこまで必要ないかもしれません。

しかし、テストは失敗するものです。 そのため、テストからのフィードバックで得られる情報は重要です。

フィードバックからの情報としては、次のような情報を得られることが重要になってきます。

  • どのように失敗したのか
  • なぜ失敗したのか
  • ソースコードのどこで失敗したのか

Xcode12ではテストの失敗時に上記のような情報をより分かりやすく提供してくれるようになっています。

ここでは次の3点について説明をしていきます。

  • テストの実行時間の制御(spindump)
  • アサーション
  • テスト失敗時の情報(XCTIssue)

テストの実行時間の制御(spindump)

テストの実行時間の制御によりテストが失敗した場合、どうして想定時間より長くかかったかを知る必要があります。

ハングした原因を推測することは難しいことが多いです。 Xcode12からテスト実行時間の制御によりテストが失敗した場合、テスト結果にspindumpが添付されるようになりました。

テスト結果のspindumpを開くことで、失敗したテストケース名があるはずです。 この情報をおうことで、最も多くの時間を費やしているメソッドを教えてくれます。

これにより、ハングした原因の調査の助けになります。

アサーション

テストが失敗した場合に、指定した期待する値と実際の値が異なっていたとして、それぞれの値がどのような意味を持つのかがわからないことがあります。

これがわかるようにアサーションメッセージを適切に使うことは重要です。 次のようにXCTAssertsではメッセージを設定できます。

XCTAssertEqual(expected, actual, "アサーションメッセージ")

このメッセージに適切な情報を含めておくことが重要です。 しかし、このメッセージに失敗したファイルパスを含める必要はありません。

Xcode12では失敗時の情報がより適切に表示されるようになりました。

例えば独自のアサーションメソッドを用意することがあると思います。 その場合、今までは次のようにテストケース側にアノテーションが付与されずに、実際に呼び出しているアサーションメソッド側にアノテーションが付与されます。

f:id:swet-blog:20200813095311p:plain

そのため、実際にどこでテストが失敗したのかがわかりづらいところがありました。 今までは、次のようにfileとlineを利用することで上記の画像の場所ではなく、テストケース側でアノテーションを表示できました。

func assertSample(file: StaticString = #file, line: UInt = #line) {
    XCTAssertTrue(false, file: file, line: line)
}

しかし、この対応でも問題は残ります。 この対応ではテストケース側にアノテーションが表示されます。 そのため、アサーションメソッド内のどのアサーションで失敗したかまではわかりません。

Xcode12ではこれらの問題が解決しています。

今回のような場合では、テストケース側にはグレイのアノテーションが表示され、アサーションメソッド側には赤いアノテーションが表示されるようになりました。

テスト失敗時の情報(XCTIssue)

Xcode12からテスト失敗時の情報が今までよりまとまっています。

今まではXCTestではテスト失敗時にrecordFailure APIを呼び出しています。 これは次にあるように4つの情報を保存しています。

func recordFailure(withDescription description: String, 
            inFile filePath: String, 
            atLine lineNumber: Int, 
            expected: Bool)

expectedはアサーションの失敗によってテストが失敗した場合はtrueで、例外の場合だとfalseになります。

Xcode12からはrecordFailureはdeprecatedになり、新しくrecord APIが追加され、このAPIが呼び出せるようになりました。

このAPIを見るとわかるように、今までのような値の渡し方ではなくXCTIssueにカプセル化されています。

そして、今までよりも複数の情報が追加されています。

これにより、自動テストを実行したXcode上や自動テストの成果物であるResult Bundleでテスト失敗時の情報がより細かく分かるようになりました。

このrecord APIはテストの失敗時に呼ばれるので、overrideしてカスタムなものを作ることもできます。

overrideできることで、情報を増やしたり絞ることもできます。 たとえば、Attachmentとしてログを別途追加するといったこともできます。

    override func record(_ issue: XCTIssue) {
        var issue = issue
        issue.add(XCTAttachment(string:  log))
        super.record(issue)
    }

Instruments

ここからは、片山がXcode12からのInstrumentsについて、業務でInstrumentsを利用している中で特に嬉しい変更について2つご紹介します。

xctraceの登場

今回Instrumentsにおいても大きな変更が入りました。 今までCLIから実行する際にはinstrumentsコマンドを用いていましたが、Xcode12でdeprecatedとなりました。 その代わりとしてxctraceコマンドが新たに追加されました。xctraceに新生したと同時に新たにできることが増えました。 そのxctraceで新たにできるようになったことで最も嬉しいと感じたのが、「Analysis Core Tables」のexportです。

Xcode11までのInstrumentsでは、計測した結果のtraceファイルを基本的にはInstruments App以外で見ることができませんでした。 そのため、計測した結果をGUIでチェックする必要がありました。 例えば端末温度を計測をした際はtraceファイルをInstrumentsで開いて、GUIを操作して問題ないかをチェックする必要があります。 (我々は、InstrumentsアプリをXCTestで動作させ、スクリーンショットやUI要素の情報を得ることで計測結果を簡易的に取得することをおこなっていました)

これらの計測結果のtraceファイルの内容をxctraceからXML形式でexportできるようになったため、exportしたXMLをパースして計測結果を機械的にチェックすることも可能になります。 毎日計測して結果を得たい場合にはとてもありがたい機能追加です。 細かい使い方についてはmanコマンドにしか詳細が無いのでぜひそちらを参照してみてください。

また、xctraceではかゆいところに手が届く変更も入りました。 instrumentsコマンドは以下のような少しだけ不便な部分がありました。

  • 選択できるtemplateの一覧をinstrumentsコマンドから見ることができない
  • 選択できる端末の一覧をinstrumentsコマンドから見ることができない

些細な問題かもしれませんが、ちょっとだけ不便なところがxctraceでは改善されました。 templateと端末の一覧をxctraceのコマンドから簡単に調べることができます。

xctraceについては当然まだベータ版であり、不具合と思われる報告もされています。 気になる方はApple Developer Forumで探してみてください。

保存 / 読み込み速度の改善

Instruments App本体でも少しうれしい改善がありました。 traceファイルは長時間計測するとサイズも大きくなっていき、保存/読み込みにかなりの時間が掛かっていました。 その問題となっていた保存/読み込みのパフォーマンスが次のように改善されました。

  • 保存時:最大40%高速化
  • 読み込み時:最大80%高速化

あくまで最大と書いてあり状況によって変化するため、私個人として試したところでは劇的に早くなったとは感じないが、少しは早くなったかなという感想です。 Resolvedの項目に記載されてるため、Appleとしても気にしていたと思われます。 今後のアップデートでも保存/読み込み速度の改善が継続的にされると嬉しいです。

おわりに

今回、WWDC2020の動画からSWET視点で選んで上述した2点について紹介しました。

WWDC2020の動画を聞いた感想として、すでにある機能が今まで以上により使いやすい形でまとめられ提供されるようになったと感じています。

また、まだXcode12がリリース前の関係で変わることもあるかと思いますし、伝えきれなかった情報もあります。 それらについては正式にリリースした時点で追加記事を書ければと思います。

参考資料

おまけ

SWETではテストに特化した勉強会としてTest Nightを定期的に開催しています。

昨今の状況もあり開催できていませんでしたが、オンラインでの開催をおこなう予定です。 それにともない、Test Nightとは別の「Test Online」というグループをconnpassで作成しています。

このグループでの勉強会を近日中にconnpassを公開するので、ぜひとも参加していただければと思います。

おまけ2

今回、Instruments周りについて紹介した理由としてパフォーマンス計測に力を入れて取り組んでいるというのがあります。

今までの取り組みについて、iOSDC Japan 2020で登壇予定ですのでぜひ視聴していただければと思います。

継続的にアプリのパフォーマンスを計測する by kariad | トーク | iOSDC Japan 2020 - fortee.jp

DroidKaigi 2020発表動画公開記念:RobolectricでUIテストを動かすのに必要なことのまとめ

こんにちは。SWETグループの外山(@sumio_tym)です。

先日、DroidKaigi 2020で発表予定だったセッション「Robolectricの限界を理解してUIテストを高速に実行しよう」 の動画がYouTubeのDroidKaigiチャンネルで公開されました。

新型コロナウイルスの影響でDroidKaigi 2020が中止になってしまったのは残念でしたが、 発表したかった内容を皆さんに伝えることができて、とても嬉しいです。

発表スライドはこちらです。

合わせてサンプルコードも公開していますので、よろしければご覧ください。

さて、本記事では「RobolectricでもUIテストを動かしてみたいけど・・・動画を見る時間がない!」という方に向けて、 ぜひ押さえておきたいポイントを厳選してお伝えします1

  • 試してみる前に知っておきたいポイント
  • テストがすぐ書ける環境を構築する
  • 工夫が必要なJetpackコンポーネント

なお「何故そうしなければならないのか」といった理由や背景についての解説は割愛しています。 その点に興味がある方は動画やスライドを参照してください。

試してみる前に知っておきたいポイント

Robolectric上でUIテストを動かそうとする前に、最低限知っておきたいポイントは次の3点です。

  • 最初はInstrumented Testで動かす
  • 動かないと分かっているのを避ける
  • ひとつの画面で完結するものから着手する

これらのポイントを事前に押さえておけば、大きな手戻りが発生するリスクを抑えられます。 「すぐに試してみたい!」という方もご一読ください。

ポイント1:最初はInstrumented Testで動かす

テストを高速に実行できるRobolectricですが、UIテスト実行における大きな弱点は「画面が無い」点です。 画面が無いため、テストコードが意図通り動作しているのか(=意図通りUIを操作しているのか)目視で確認できません。

そのため、同じテストコードをInstrumented Testでも動かせるようにしておきましょう。 Instrumented Testであれば、テストの動作状況を画面を見ながら確認できます。

特に、テストコードを書いている途中では、画面を目視しながらの動作確認は必須と言えます。 最初はInstrumented Testで動くようにテストを書き、その後にRobolectricでも動くようにしていく方法がおすすめです。 テストコードの具体的な配置方法については後で紹介します。

ポイント2:動かないと分かっているものを避ける

発表時点の調査で、Robolectricで意図通り動かないと分かっているものは次の通りです。

Robolectricで動かすUIテストでは、これらの操作は避けましょう。

ポイント3:ひとつの画面で完結するものから着手する

事前に動かない操作を知っていたとしても、テストを書き進めると意図せずそのような操作に直面してしまうことがあります。 そのリスクを避けるために、できるだけ操作するステップが少ないテストから書き始めましょう。 複数の画面をまたがるテストだと操作ステップが増えがちなので、ひとつの画面で完結するものから始めるのがおすすめです。

テストがすぐ書ける環境を構築する

事前に知っておきたいポイントを押さえたところで、テストがすぐ書ける環境を構築していきます。 既にプロダクトコードをAndroid Studioでビルドできる環境があることを前提とします。

ここで説明する手順に沿って構築すれば、次のすべてが揃った環境を入手できます。

  • IdlingResourceに対応するように筆者が改変したRobolectric
  • DataBindingの非同期処理を待ち合わせるDataBindingIdlingResource2
  • Architecture Componentのバックグラウンドスレッドを待ち合わせるTaskExecutorWithIdlingResourceRule
  • Instrumented TestとRobolectricが動作するLocal Testでテストコードを共有できるShared Test

手順1:必要なファイルをコピーする

サンプルコードをcloneし、次のディレクトリをご自身のプロジェクトにコピーします。 そのときに、コピー先も同じディレクトリ構成にしてください。 たとえばapp/src/test/java/androidxディレクトリは、 ご自身のプロジェクト側でもapp/src/test/java/androidxディレクトリとしてコピーしてください3

  • app/local-repo
  • app/src/test/resources
  • app/src/test/java/androidx
  • app/src/sharedTest/java/com/android/example/github/util
  • app/src/sharedTest/java/com/example/android/architecture/blueprints/todoapp/util

手順2:build.gradleに追記する

app/local-repoディレクトリを、Maven形式のリポジトリ参照先として追加します。 app/build.gradleに、次のように追記してください。

repositories {
    maven { url = file('local-repo') }
}

トップレベルのbuild.gradleに書くこともできます。 その場合はfile('app/local-repo')のように、local-repoディレクトリの相対パスが正しくなるように注意してください。

次に、Robolectricを使えるようにするためのandroid.testOptions.unitTests.includeAndroidResourcestrueにセットします。 app/build.gradleに、次のように追記してください

android {
    ...
    testOptions {
        unitTests.includeAndroidResources = true
        ...
    }
}

次に、Shared Testを置くapp/src/sharedTestディレクトリをInstrumented TestとLocal Test両方のソースセットに加えます。 app/build.gradleに、次のように追記してください。

android {
    ...
    sourceSets {
        androidTest {
            java.srcDirs += file('src/sharedTest/java')
        }
        test {
            java.srcDirs += file('src/sharedTest/java')
        }
    }
}

最後に、依存関係に必要なライブラリを追加します。 Robolectricはapp/local-repoのものを参照する必要があるので、バージョン表記を4.3.1-modifiedとしてください。 なお、このRobolectricはEspressoのIdlingResourceに対応するように筆者が改変したものです。詳しくはスライドの34〜57ページを参照してください。

dependencies {
    ...

    androidTestImplementation "androidx.test:core-ktx:1.2.0"
    androidTestImplementation "androidx.test.ext:junit-ktx:1.1.1"
    androidTestImplementation "androidx.test.espresso:espresso-contrib:3.2.0"
    androidTestImplementation "androidx.test.espresso.idling:idling-concurrent:3.2.0"
    androidTestImplementation "androidx.arch.core:core-testing:2.0.0"
   
    testImplementation "org.robolectric:robolectric:4.3.1-modified"
    testImplementation "androidx.test:core-ktx:1.2.0"
    testImplementation "androidx.test.ext:junit-ktx:1.1.1"
    testImplementation "androidx.test.espresso:espresso-contrib:3.2.0"
    testImplementation "androidx.test.espresso.idling:idling-concurrent:3.2.0"
    testImplementation "androidx.arch.core:core-testing:2.0.0"
}

これらのモジュールが提供する主な機能は次の通りです。

モジュール 主な提供機能
androidx.test:core-ktx Activityの起動を伴うテスト
androidx.test.ext:junit-ktx AndroidJUnit4
androidx.test.espresso:espresso-contrib Espresso
androidx.test.espresso.idling:idling-concurrent EspressoのIdling Resource
androidx.arch.core:core-testing Android Architecture Componentのテスト
org.robolectric:robolectric Robolectric

Robolectric以外のモジュールは、Local TestとInstrumented Testの両方で使うため、 androidTestImplementationtestImplementationで宣言します。 RobolectricはLocal Testだけで使いますので、testImplementationのみで宣言します。

手順3:テストクラスを用意する

テストクラスは、Instrumented Test向け・Local Test向けのものをそれぞれ用意します。 ここで紹介する内容をコピー&ペーストして、クラス名とテスト対象Activity名を置換すれば、すぐに使い始められます。

Instrumented Test向けのテストクラス

Instrumented Test向けの典型的なテストクラス定義は次の通りです。 このクラス定義をapp/src/androidTestに置いてください。

import androidx.test.espresso.IdlingRegistry
import androidx.test.ext.junit.rules.activityScenarioRule
import androidx.test.ext.junit.runners.AndroidJUnit4
import com.android.example.github.util.TaskExecutorWithIdlingResourceRule
import com.example.android.architecture.blueprints.todoapp.util.DataBindingIdlingResource
import com.example.android.architecture.blueprints.todoapp.util.monitorActivity
import org.junit.After
import org.junit.Before
import org.junit.Rule
import org.junit.Test
import org.junit.runner.RunWith

@RunWith(AndroidJUnit4::class)
class MyActivityTest {

    @get:Rule
    val activityScenarioRule = activityScenarioRule<MyActivity>()

    @get:Rule
    val taskExecutorWithIdlingResourceRule = TaskExecutorWithIdlingResourceRule()

    private val dataBindingIdlingResource = DataBindingIdlingResource() // ★

    @Before
    fun setUp() {
        val idlingRegistry = IdlingRegistry.getInstance() // ★
        dataBindingIdlingResource.monitorActivity(activityScenarioRule.scenario) // ★
        idlingRegistry.register(dataBindingIdlingResource) // ★
    }

    @After
    fun tearDown() {
        IdlingRegistry.getInstance().unregister(dataBindingIdlingResource) // ★
    }

    @Test
    fun myTest() {
        // app/src/sharedTest/java にあるテストコード共通部分を呼び出す
    }
}

これを雛形にすれば、AAC (Android Architecture Components)が使われたアプリのテストはだいたいカバーできると思います。 なお、★印を付けたdataBindingIdlingResourceに関係する処理は、Data Bindingを使っていない場合は不要です。

Local Test向けのテストクラス

次はLocal Testにおけるテストクラス定義です。 このクラス定義はapp/src/testに置いてください。

import androidx.test.espresso.IdlingRegistry
import androidx.test.ext.junit.rules.activityScenarioRule
import androidx.test.ext.junit.runners.AndroidJUnit4
import com.android.example.github.util.TaskExecutorWithIdlingResourceRule
import com.example.android.architecture.blueprints.todoapp.util.DataBindingIdlingResource
import com.example.android.architecture.blueprints.todoapp.util.monitorActivity
import org.junit.After
import org.junit.Before
import org.junit.Rule
import org.junit.Test
import org.junit.runner.RunWith
import org.robolectric.annotation.LooperMode

@RunWith(AndroidJUnit4::class)
@LooperMode(LooperMode.Mode.PAUSED)
class RobolectricMyActivityTest {

    @get:Rule
    val activityScenarioRule = activityScenarioRule<MyActivity>()

    @get:Rule
    val taskExecutorWithIdlingResourceRule = TaskExecutorWithIdlingResourceRule()

    private val dataBindingIdlingResource = DataBindingIdlingResource() // ★

    @Before
    fun setUp() {
        val idlingRegistry = IdlingRegistry.getInstance() // ★
        dataBindingIdlingResource.monitorActivity(activityScenarioRule.scenario) // ★
        idlingRegistry.register(dataBindingIdlingResource) // ★
    }

    @After
    fun tearDown() {
        IdlingRegistry.getInstance().unregister(dataBindingIdlingResource) // ★
    }

    @Test
    fun myTest() {
        // app/src/sharedTest/java にあるテストコード共通部分を呼び出す
    }
}

ほとんどInstrumented Testと同じですが、以下の点に注目してください。

  • テストクラス名がInstrumented Testのものと違う
    現状では、app/src/androidTestapp/src/testで同じ名前のクラスを定義するとAndroid Studio上でエラーになってしまいます(バージョン3.6.3で確認)。 エラーを無視してビルドはできるものの、IDE上でエラーのままコードを書いていくのは苦痛です。 テストクラス名は別の名前にすることを推奨します。
  • @LooperModeアノテーションが付いている
    Robolectricのタスクスケジューラの種類をPAUSEDにしています。 詳しく知りたい方はスライドの22〜26ページを参照してください。

こちらも、★印を付けたdataBindingIdlingResourceに関係する処理は、Data Bindingを使っていない場合は不要です。

手順4:Instrumented Test・Local Test両方から呼びだせるようにテストを書く

手順3で作成したテストクラスにおける、テストの種類とテスト実行時に呼び出されるテストメソッドの関係は次のようになります。

テストの種類 テスト実行時に呼び出されるテストメソッド
Instrumented Test MyActivityTestクラスのmyTestメソッド
Local Test RobolectricMyActivityTestクラスのmyTestメソッド

これら2つのmyTestメソッドに同じテストコードを書けば、両者から同じテストを実行できるようになります。 とはいえ、両方のメソッドに同じコードを書くとコードが重複しメンテナンス性の低下を招きます。 その事態を避けるために、テストコード本体はapp/src/sharedTestに配置し、 myTestメソッドからはテストコード本体を呼び出すだけにします。

例えば、app/src/sharedTestに配置したテストコード本体をdoMyTest()関数としましょう。

// app/src/sharedTestに配置する
fun doMyTest() {
    Espresso.onView(...).perform(click())
    Espresso.onView(...).check(isDisplayed())
    ...
}    

その場合2つのmyTestメソッドでは、コード重複をできるだけ抑えるためにdoMyTest()を呼び出すだけとします。

// app/src/androidTestに配置する
...
class MyActivityTest {
    ...
    @Test
    fun myTest() {
        doMyTest()
    }
}    
// app/src/testに配置する
...
class RobolectricMyActivityTest {
    ...
    @Test
    fun myTest() {
        doMyTest()
    }
}    

この例におけるdoMyTest()部分の設計パターンはPage Objectデザインパターンがおすすめです。 Page Objectデザインパターンの詳細については割愛しますが、本パターンを適用するとmyTestメソッドの本体は次のような感じになります。

fun myTest() {
    MyGardenPage
            .goPlantList()
            .showPlantDetail("Mango")
            .addToMyGarden()
            .goBackPlantList()
            .goMyGarden()
            .assertPlanted("Mango")
}

スッキリ見通しが良くなりますね。

Page Objectについて詳しく知りたい方は、 DeNA CodelabsでSWETが公開している 「Espressoの知識ゼロでも書ける!Android UIテストはじめの一歩」に挑戦してみてください。

補足:テストクラスも共通化する方法

ここで紹介した方法ではmyTestメソッド内のコード重複は避けられません。

その重複も回避したい場合、本記事で紹介した範囲であれば2つのテストクラスを共通化することもできます。

その場合はLocal Test向けのテストクラスだけをapp/src/sharedTestに置きます。 app/src/androidTestapp/src/testには対応するテストクラスは置かないでください。

そして、app/build.gradleにInstrumented Testの依存関係としてorg.robolectric:annotationsを追加します。

dependencies {
    ...
    androidTestImplementation "org.robolectric:annotations:4.3.1"
}

Robolectricのアノテーションの違いだけであれば、この方法でテストクラスを共通化できます。 ただし、筆者個人の意見としては、あまりこの方法はおすすめしません。 おすすめしない理由は、両者のテスト間で完全に同じコードを維持できない可能性が高いと考えるからです。

たとえば、RobolectricのShadowクラスを使いたくなる場合など、どうしても共通化できない部分がでてきたとします。 そうなった場合、共通化できない部分をapp/src/androidTestapp/src/testへ切り出すことになります。

// app/src/sharedTestに配置したコード
@Test
fun myTest() {
  ...
  doActionOnlyLocalTest() // Local Testでしか実行したくない処理
}

// app/src/testに配置したコード
fun doActionOnlyLocalTest() {
  // ここにLocal Testでしか実行したくない処理を書く
}

// app/src/androidTestに配置したコード
fun doActionOnlyLocalTest() {
  // 何も書かない
}

ところがこの方法を取ってしまうと、前述した 「app/src/androidTestapp/src/testで同じ名前のクラスを定義するとAndroid Studioでエラーになる」 というAndroid Studioの振舞いに抵触してしまいます。 エラーを無視してビルドはできるものの、現状ではおすすめするのが難しいです。

将来Android Studioの振舞いが改善されたら、この方法がベストな選択肢になると思います4

工夫が必要なJetpackコンポーネント

Jetpack Componentのうち、RoomWorkManagerでは更なる対応が必要です。 その対応方法を説明します。

Room

Roomを使うアプリのうち、RoomDatabase(のサブクラス)への参照をstaticなフィールド(Kotlinのcompanion objectなどを含む)に保持しているケースが問題になります。 問題となる理由は、Robolectricの次のような振舞いと相性が良くないからです。

  • テストごとに(ひとつのテストメソッド実行の度に)SQLiteのデータベースファイルが新規に作られる
  • テストをまたいでもstaticな変数は初期化されない

RoomDatabaseのインスタンスは、データベースファイルと一対一対応しているため、 データベースファイルが作り直されたときは改めてインスタンスを作り直す必要があります。 また、RoomDatabaseのインスタンスが変わるとDAOのインスタンスも変わってしまう点にも注意が必要です。

そのため、そのようなアプリをRobolectricでテストするときは、テストのセットアップ時に次の処理を行うようにしましょう。

  1. RoomクラスのdatabaseBuilderメソッドを使って、RoomDatabaseインスタンスを作り直す
  2. アプリ内で保持している古いRoomDatabaseへの参照を、作り直したインスタンスへの参照に更新する
  3. 同様に古いDAOインスタンスへの参照を、新しいRoomDatabaseから取得し直したDAOインスタンスへの参照に更新する

RoomDatabaseの初期化をアプリケーションクラスで行っている場合は、Robolectric用に別のアプリケーションクラスを用意するのが簡単です。 Robolectricではテストクラスに次のようなアノテーションを指定できます。

@Config(application = TestApplication::class)
class RobolectricMyActivityTest { ... }

これで、Robolectricはこのアノテーションで指定されたアプリケーションクラスを使って初期化するようになります。 この例ではTestApplicationクラスのonCreateメソッドが呼び出されるようになりますので、 そのonCreateメソッドの中でRoomDatabaseインスタンスを作り直すなどの処理をすると良いでしょう。 なお、Robolectricではアプリケーションクラスの初期化もテストごとに行われます。

テスト対象アプリによって事情が異なるため具体的なコード例は割愛しますが、 Android Sunflowerアプリの修正例をスライド70〜75ページに掲載していますので、あわせて参考にしてください。

WorkManager

WorkManagerのデフォルトの振舞いでは、未完了のWorkはアプリが終了しても消えることがありません。 次回アプリ起動時に再開されます。

そのようなWorkの特徴により、前回のテストで未完了だったWorkが次のテストで意図せず起動することがあります。 その事態を回避するためにはWorkManagerTestInitHelperを使います。具体的な手順を見ていきます。

まず、app/build.gradleにLocal Testの依存関係としてandroidx.work:work-testingを追加します。

dependencies {
    ...
    testImplementation "androidx.work:work-testing:2.3.1"
}

次に、app/src/test/AndroidManifest.xmlを次の内容で作成します。

<manifest xmlns:android="http://schemas.android.com/apk/res/android"
    xmlns:tools="http://schemas.android.com/tools">

    <application>
        <provider
            android:name="androidx.work.impl.WorkManagerInitializer"
            android:authorities="${applicationId}.workmanager-init"
            tools:node="remove" />
    </application>

</manifest>

既にファイルが存在する場合は<provider>部分を<application>タグの中に追記してください。

最後に、テストのセットアップフェーズで、次のようにWorkManagerを初期化します。 Roomのケースと同様にテスト用アプリケーションクラスのonCreateメソッドで初期化するのが良いと思います。

class TestApplication : Application() {
    override fun onCreate() {
        ...
        WorkManagerTestInitHelper.initializeTestWorkManager(this)
        ...
    }
}    

テスト用アプリケーションクラスを用意する場合は、忘れずにテストクラス側でアプリケーションクラスを指定するようにしましょう。

@Config(application = TestApplication::class)
class RobolectricMyActivityTest { ... }

この対応で、未完了だったWorkが起動することはなくなります。 また、起動したWorkが同期的に実行されるようにもなるので、UIテストの安定化に寄与するはずです。

おわりに

RobolectricでUIテストを動かすときのポイントを紹介しました。 これらを実践すれば、UIテストの大部分がRobolectricでも動作するようになっていることと思います。

是非、簡単なところから少しずつ書きはじめてみてみてください!


  1. この文脈における「UIテスト」は、EspressoのAPIを使ったテストとします

  2. このコードは孫FragmentにDataBindingが使われているケースをサポートしていませんでした。サンプルコードではその問題を修正しています

  3. 特にapp/src/test/java/androidx配下のクラスは、パッケージ名を変更すると動かなくなりますので注意してください。app/src/sharedTest配下のクラスについては、パッケージ名を変更した上で別のディレクトリに配置しても問題ありません

  4. 途中から違う事象について議論しているので確証はありませんが、Issue 140375151が関連するバグチケットのようです

ゼロから学んだ形式手法

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

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

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

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

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

f:id:swet-blog:20200407164509j:plain

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

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

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

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

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

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

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

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

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

\exists LocalVariables. \exists LocalVariables'. PredLocal \land PredPromote

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

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

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

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

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

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

今の理解

f:id:swet-blog:20200407164516j:plain

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

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

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

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

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

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

f:id:swet-blog:20200407164522j:plain

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

形式手法は役に立つ!

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

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

デザイン電卓として

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

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

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

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

f:id:swet-blog:20200407164529j:plain

仕様の妥当性確認として

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

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

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

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

より積極的な適用として

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

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

おまけの副産物

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

たとえば契約による設計は「オブジェクト指向入門」12でバートランド・メイヤーが唱えた概念ですが、その由来が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日(木)に一部のセッションをライブ配信しました。

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

発表内容

タイトル

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

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

セッション情報

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

資料

動画

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での質問

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

有向です。

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

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

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

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

我々が初めて形式仕様記述したプロダクトは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)にてお届けしています。ぜひフォローをお願いします!

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 と呼びます1Advanced 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などのコードは一部省略しています)。 emailnameの値を受け取り、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と同じように関数の引数でタイムスタンプを取得する関数を渡すか、 プログラミング言語Go2 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を使います。

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

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は、ローカルの事前・事後を表す変数LocalVariablesLocalVariables'、ローカルの操作を表す述語PredLocal、ローカルとグローバルの状態の関係を表す述語PredPromoteを使い、次の形で表現されます。

\exists LocalVariables. \exists LocalVariables'. PredLocal \land PredPromote

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

本記事の題材

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

f:id:swet-blog:20200214112532p:plain

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

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

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

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

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

f:id:swet-blog:20200219113009p:plain

事前のシステムの状態をs、事後のシステムの状態をs'と表現しています。 ブランチbsに紐付けられたブランチです。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はローカルな操作・ローカルとグローバルの状態の関係を表す述語でグローバルな操作を表現する書き方です。

\exists LocalVariables. \exists LocalVariables'. PredLocal \land PredPromote

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]
    }
}

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

f:id:swet-blog:20200214112559p:plain

コミットとファイルに関わるローカルな操作(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以外のブランチ(グレーのゾーン)が変化しないということです。 また、promoteCommitToSystemcがどのように変化するかは関与しません。 そのためpromoteCommitToSystemは他のローカル操作でも再利用ができます。

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

同値であることを確認

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の中のcommitNewFileLocalpromoteCommitToSystemを定義で置き換えてみます。

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が束縛する変数cc = b.(s.bc)なので、一点規則と呼ばれる次の規則が適用できます。

(\exists x. x = a \land P(x))  \Leftrightarrow  P(a)

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

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を検討してみると良いかもしれません。

参考