App Crash LabをAlloyとDbCの視点で読む
はじめに
@aichance さんが開発したApp Crash Labという、ローカルWebアプリの保存データを検査するツールを知りました。
解説や設定例を読んでいて、最初は「JSONでテストケースを書くツールかな」と思いました。しかし、何をJSONに書くのかを見ていると、普段使っているAlloyや、Design by Contractの考え方に近いものを感じました。
正常な状態を確立する。その状態で操作する。操作の結果を確認する。そして、変わってはいけないものが守られたかを確かめる。
この視点で読むと、App Crash Labの設定は、操作手順とともにシステムが満たすべき契約を記述するものに見えてきます。
本記事では、App Crash Lab 0.7.0の設定形式を題材に、その共通点と違いを考えます。
保存しましたの先を検査する
App Crash Labは、正常に保存できる操作を起点に、主に次のことを検査します。
- 再読み込み後も、選択した保存値が維持されること
- 無効な更新が拒否された後も、元の保存値が維持されること
- 明示的に設定した場合、実際に出力したJSONバックアップを空のブラウザ環境へ復元し、再読み込み後も値が一致すること
内部ではPlaywrightを使います。実行時にLLMを呼ぶ仕組みではなく、操作や期待値は利用者がJSONで指定します。
たとえば、メモを保存するアプリを考えます。
「Buy coffee」と入力して保存すると、「Saved」と表示される。ここまでは成功したように見えます。
では、ページを再読み込みしたらどうなるでしょうか。空のメモを保存しようとしてエラーになった後は、元のメモが残っているでしょうか。
保存操作が一度成功したことと、その後も正しい状態が守られることは、別々に確認する必要があります。
JSONに書くのは操作と条件
公式のNotesサンプルには、次のような設定があります。以下は説明用の抜粋で、単独では実行できません。
{
"setup": [
{ "action": "fill", "target": { "label": "Note" }, "value": "Buy coffee" },
{ "action": "click", "target": { "role": "button", "name": "Save" }, "save": true },
{ "action": "expectText", "target": { "testId": "status" }, "value": "Saved" }
],
"observe": {
"savedNote": { "source": "text", "target": { "testId": "saved" } }
},
"expected": {
"savedNote": "Buy coffee"
}
}
setupは、正常な保存状態を作る手順です。expectedで、その保存が既知の正常値に到達したことを確認します。observeは、その後も比較する対象です。
無効な更新は、別に記述します。
{
"rejectedUpdate": {
"steps": [
{ "action": "fill", "target": { "label": "Note" }, "value": "" },
{ "action": "click", "target": { "role": "button", "name": "Save" } }
],
"observe": {
"message": { "source": "text", "target": { "testId": "status" } }
},
"expected": {
"message": "Rejected: note is empty"
}
}
}
ここには二つの要求があります。
「空のメモは拒否されること」と、「拒否された後も保存済みメモは変わらないこと」です。
エラー表示は変化してよい。一方、保存済みデータは変化してはいけない。何を変えてよく、何を守るのかが分けて書かれています。
DbCの視点で読み替える
Design by Contractでは、事前条件、事後条件、不変条件によって、ソフトウェアが満たすべき条件を表現します。
App Crash Labの設定も、この言葉で整理すると理解しやすくなります。
| App Crash Labで記述するもの | 契約としての読み方 |
|---|---|
| setupとexpected | 検査の前提となる正常な保存状態を作り、成立を確認する |
| rejectedUpdate.steps | 契約を確認したい操作を具体化する |
| rejectedUpdateのobserveとexpected | 無効な操作が拒否されたという事後の条件を確認する |
| トップレベルのobserve | 操作の前後で維持すべき状態を選ぶ |
ただし、これは一対一の対応ではありません。setup自体は条件式ではなく操作手順です。また、通常のDbCでいう事前条件は呼出し側が満たすべき条件ですが、ここで確認しているのはテストの基準状態です。
無効入力の検査にも違いがあります。事前条件に違反した呼出しについて何を保証するかは、その契約によります。Webアプリが無効入力を受け取ることを想定し、「拒否し、保存状態を維持する」と定めるなら、それは拒否処理の契約として考えられます。
そのうえで、私は特に、保存状態を操作前の値と比較する部分にDbCとの近さを感じました。事後条件の中で、操作前の値を参照するoldのような見方ができます。
不変条件というより状態を維持する契約
ここは少し丁寧に区別したいところです。
一般に不変条件というと、「在庫数は0以上」のように、各状態が満たす性質を考えます。一方、「拒否された更新の前後で保存値が等しい」は、二つの状態の関係です。
概念的には、次のように書けます。
正常に保存された状態 s で無効な更新を行う
→ 更新が拒否される
→ saved(s_after) = saved(s_before)
これは事後条件として表せますし、変更してはいけない領域を指定するフレーム条件にも近い話です。
observeは、その比較に使う状態を選びます。アプリ全体が何一つ変化しないと要求するのではなく、保存済みメモなど、維持すべき部分に注目します。
この区別があるため、エラー表示が変わることと、保存済みデータが変わらないことを同時に扱えます。
Alloyと近いと感じたところ
私はAlloyで設計するとき、「何ができるか」と一緒に、「どの遷移でも何を壊してはいけないか」を考えます。
たとえば、自作のサイネージGlyphaでは、「失敗が成功した表示を置き換えてはならない」という条件を大切にしています。
App Crash LabにはGlypha向けの設定例もあります。正常なシーンを公開した後、再読み込みと、HTTP 422で拒否される無効な更新を行い、/displayのJSONとETagが維持されるかを比較します。
この例を見たとき、Alloyで考えていた状態遷移の性質を、実際のアプリで観測できる値へ落とし込んだものとして理解できました。
ただし、AlloyとApp Crash Labでは、確かめる対象も方法も違います。
| 観点 | Alloy | App Crash Lab |
|---|---|---|
| 対象 | 抽象化したモデル | 実行中のアプリ |
| 条件の表現 | 論理式、関係、遷移など | 操作、観測対象、期待値を記述したJSON |
| 確認方法 | 指定した解析範囲などの条件下で反例を探索 | 指定した具体的な操作を実行して値を比較 |
| 問題が見つかったとき | モデル上の反例 | 実アプリの差分、実行段階、再現用テストなど |
Alloyでモデルが満たす性質を調べても、実装がそのモデルに従うことは別に確認する必要があります。App Crash Labで一つの操作がPASSになっても、すべての入力や遷移について成立するとは限りません。
両者をつなぐには、「モデル上の状態を、実装のどこで観測するか」という対応付けが必要になります。
何を観測するかを決める作業
JSONの設定例を読んで、書くのは結構大変そうだとも感じました。
保存ボタンのselectorを探すだけでは終わりません。保存完了とは何か。保存済みデータはどこにあるか。拒否が完了したことを、何で確認するか。正常に変化する値と、維持する値をどう分けるか。
これらを決めるには、アプリの仕様を理解する必要があります。
たとえば、入力欄に「Buy coffee」が残っていても、永続化されたメモは消えているかもしれません。localStorageに言語設定が残っていても、画面の表示言語は戻っているかもしれません。
どちらを観測するかによって、同じアプリでも検査結果の意味は変わります。
この難しさは、Alloyでモデルの境界を決めたり、DbCで何を保証するかを決めたりする作業と似ています。条件を実行可能な形にするには、先に何を正しいとするかを考えなければならない。
JSONの作成はエージェントに手伝ってもらえます。それでも、観測対象や期待値が意図した契約を表しているかは確認する必要があります。
判定不能を成功にしない
App Crash Labには、PASSとFAILのほかにINCONCLUSIVEがあります。
正常な保存状態を確認できなかった、必要な値を観測できなかった、といった場合には、信頼できる判定ができません。
前提が成立しているのか分からないのに、「壊れていることは確認できなかったから成功」と扱わないわけです。
これは、条件そのものと同じくらい重要に感じました。契約を書くだけでなく、その契約を評価できる状況だったかまで扱っています。
なお、検査は設定した手順と観測時間の範囲で行われます。既定では期待状態への到達後に250msの安定性確認を行いますが、あらゆる一時的変化や長時間後の故障、電源断を網羅するものではありません。
おわりに
App Crash Labを読んで面白いと感じたのは、保存後の操作に対して「何が成立し、何が維持されなければならないか」を明示する構成でした。
もちろん、同じ検査はPlaywrightで直接書けます。通常のテストにも事前条件や事後条件は含まれます。契約という考え方がApp Crash Labだけのものというわけではありません。
それでも、正常状態、拒否の確認、保存状態の維持を分けて記述する形式は、何を確かめたいのかを整理する助けになります。
普段AlloyやDbCを使っている人なら、「この操作の後に何が見えるか」に加えて、「この操作でも何が守られるべきか」という問いから読むと、App Crash Labを理解しやすいのではないかと思います。