⏰
Widgetテストを超えて: LTL/MTLでFlutterのタイミング＆順序バグを捉える

rizumita
2025/05/01に公開
 1. 導入: Flutterテストにおける「時間」という挑戦Flutterを使えば、モバイル、ウェブ、デスクトップ向けの美しいネイティブアプリケーションを、単一のコードベースから構築できます。私たちは、リッチなアニメーション、スムーズなトランジション、レスポンシブなインタラクションを備えた動的なユーザーインターフェースを作成します。しかし、このようなスムーズな体験の裏側には、テスト戦略において課題となる複雑さが潜んでいることがよくあります。それが時間という要素です。
考えてみてください。ローディングインジケーターがデータ表示前に常に表示され、その後速やかに消えることを厳密に検証するにはどうすればよいでしょうか？スナックバーのシーケンスが正しい順序で、正しい期間表示されることをどう保証しますか？状態遷移中の微妙なUIのちらつきや、操作が特定の時間枠内に完了することを保証するにはどうしますか？
Flutterにおける従来のウィジェットテストは、UIの最終状態を検証したり、特定の瞬間のプロパティをチェックしたりするのに優れています。しかし、状態のシーケンス、イベントの順序、そしてそれらの間のタイミング関係に関するプロパティをアサートすることにはしばしば苦労します。pumpAndSettleや手動チェックを含む複雑なテストを書くかもしれませんが、これらは脆くなりやすく、必ずしも時間的な全体像を捉えられるわけではなく、一時的なバグや競合状態を見逃す可能性があります。
ここで**Temporal Logic（時相論理）**が登場します。これは、時間とともに変化するプロパティについて推論するために特別に設計された形式的な手法です。単なるスナップショットを見るだけでなく、Temporal Logicは、アプリケーションの振る舞いの状態シーケンス全体、つまりタイムラインについて正確な記述を行うことを可能にします。
この記事では、Temporal Logicの能力をFlutterのテストワークフローに直接活用するために設計されたDartパッケージスイート（temporal_logic_flutter, temporal_logic_core, temporal_logic_mtl）を紹介します。これにより、これまでのテストでは見逃しがちだった種類のバグを捉え、より堅牢で信頼性の高いアプリケーションを構築することが可能になります。

 2. Temporal Logicとは？ (シンプルに！)Temporal Logic（時相論理）と聞くと難しく感じるかもしれませんが、基本的な考え方は非常に直感的です。物事が時間軸の中で互いにいつ起こるかを記述するための、形式的な語彙を提供します。Flutterのテストという文脈では、主に次の2種類のTemporal Logicが重要になります：

 Linear Temporal Logic (LTL): 「いつ」の論理LTLは、イベントや状態の順序とシーケンスを指定するものと考えてください。正確な秒やミリ秒ではなく、「前」「後」「常に」「いつか」「〜まで」といった概念を扱います。
LTLを使うと、次のような性質を表現できます：
「ユーザーがログインしている場合、プロフィールアイコンは常に表示される」（不変条件）
「リクエストが送信された場合、いつか成功メッセージまたはエラーメッセージのいずれかが表示されなければならない」（生存特性 - 何かが最終的に起こらなければならないこと）
「データがロードされるまで、ローディングスピナーは表示され続けなければならない」（特定のシーケンス制約）
「'保存'をタップした後、次の状態は'保存中...'を表示しなければならない」（直接的な結果）
LTLは、ユーザーのアクションや他のイベントに応じて、アプリケーションが正しい状態のシーケンスをたどることを検証するのに役立ちます。

 Metric Temporal Logic (MTL): 「どのくらい」を追加するMTLは、LTLに量的な時間制約を追加することで拡張します。実際の期間を含むプロパティを指定することができます。
MTLを使うと、より正確なタイミング要件を表現できます：
「メッセージを送信した後、'配信済み'ステータスは5秒以内に表示されなければならない」
「スプラッシュスクリーンは少なくとも2秒間、しかし4秒を超えない時間表示されなければならない」
「ユーザーがボタンを押し続けると、アクションはちょうど1秒後にトリガーされる」
MTLは、操作の実時間での期間やUI更新のタイミングが、ユーザーエクスペリエンスやアプリケーションの正当性にとって重要である場合に不可欠です。
ポイント: 今すぐ形式的な記号や複雑な意味論を覚える必要はありません。重要なのは、これらの論理が、Dartテスト内で複雑な時間的要件を明確かつ検証可能な方法で記述することを可能にする特定の演算子（always、eventually、next、until、およびそれらの時間制約付き版など）を提供することです。

 3. temporal_logic_flutter スイートの紹介Temporal Logicの理論と実践的なFlutterテストとの間のギャップを埋めるため、以下のDartパッケージスイートを開発しました：

packages/temporal_logic_core: これは基盤となるパッケージです。論理式（And、Or、Not、Impliesなど）を表すためのコアデータ構造、基本的なLTL演算子（Always、Eventually、Next、Until、Release）、そしてこれらの式をトレース（状態のシーケンス）に対して評価する概念を提供します。

packages/temporal_logic_mtl: temporal_logic_coreを基盤として、このパッケージはMetric Temporal Logic (MTL) を実装します。時間制約付き演算子（AlwaysTimed、EventuallyTimed）とTimeIntervalクラスを導入し、「5秒以内」のような量的な時間制約を持つ式を指定・チェックできるようにします。

packages/temporal_logic_flutter: これはFlutter開発者向けの統合レイヤーです。flutter_test内で使用するための重要なユーティリティを提供します：

TraceRecorder: テスト中にアプリケーション状態のスナップショット（AppSnap）のシーケンスを時系列で簡単にキャプチャするためのヘルパークラス。

satisfiesLtl / satisfiesMtl マッチャー: expect(trace, satisfiesLtl(formula)) のように使用して、記録されたトレースに対して時間的プロパティを明確かつ簡潔に検証できるカスタムflutter_testマッチャー。

このパッケージスイートの主な目標は、複雑な時間的振る舞いの定義と検証を、Flutterのテストプロセスに自然かつ効果的に組み込むことです。

 4. 主要概念の実践: ログインフローの検証理論だけでは分かりにくいので、実際にどのように機能するのか見ていきましょう。リポジトリに含まれるlogin_flow_ltlの例（examples/login_flow_ltl）を使用して、典型的な非同期ログインシーケンスを検証する方法を示します。
メール/パスワードフィールドとログインボタンがあるシンプルなログイン画面を想像してください。ログインに成功すると、ユーザーはホーム画面にナビゲートされます。このプロセスには、非同期処理（ネットワーク呼び出しなど）、ローディング状態の表示、および潜在的なエラー処理が含まれます。

 ステップ 1: 状態スナップショットの定義 (AppSnap)まず、任意の瞬間のアプリケーション状態のうち、関心のある部分を表す方法が必要です。ウィジェットツリー全体や完全な状態管理クラスをそのまま使う必要はありません。慣例的にAppSnapと呼ばれる、焦点を絞った不変のスナップショットクラスを作成します：
// 関心のあるアプリケーション状態のスナップショットを表します。
// 不変であり、==/hashCodeを実装する必要があります（例：equatableを使用）。
class AppSnap {
  final bool isLoading;
  final bool isOnHomeScreen;
  final bool hasError;
  final bool loginClicked; // イベント発生を示す一時的なフラグ

  AppSnap({
    required this.isLoading,
    required this.isOnHomeScreen,
    required this.hasError,
    required this.loginClicked,
  });

  // 実際のアプリ状態（例：RiverpodのNotifierが管理する状態）から作成するファクトリ
  factory AppSnap.fromAppState(AppState state, {bool loginClicked = false}) {
    return AppSnap(
      isLoading: state.isLoading,
      isOnHomeScreen: state.currentScreen == AppScreen.home,
      hasError: state.errorMessage != null,
      loginClicked: loginClicked, // イベント発生をキャプチャ
    );
  }
  // == と hashCode を実装... (Equatableパッケージの使用を推奨)
}

キーポイント:

関連性: ログイン検証に必要な情報（ローディング状態、現在の画面、エラーステータス、クリックイベント発生を示す特殊フラグ）のみを含みます。

不変性: すべてのフィールドはfinalです。

ファクトリ: ファクトリメソッドfromAppStateは、実際のアプリケーション状態（Riverpod、Blocなどが管理するAppState）を、この単純化されたスナップショットに変換します。これにより、スナップショットの正確性が保たれ、状態ロジックの重複が避けられます。

Equatable: ==とhashCodeを正しく実装することで、評価中の信頼性の高い比較が可能になります。

 ステップ 2: トレースの記録 (TraceRecorder)次に、temporal_logic_flutterのTraceRecorderを使用して、テスト中にAppSnapのシーケンス（トレース）をキャプチャします。
import 'package:temporal_logic_flutter/temporal_logic_flutter.dart';
import 'package:flutter_riverpod/flutter_riverpod.dart'; // または使用している状態管理パッケージをインポート

// testWidgets内...
final recorder = TraceRecorder<AppSnap>();
final container = ProviderContainer(); // Riverpodを使用する場合
addTearDown(container.dispose);

// 時間追跡を開始し、以前のトレースをクリア
recorder.initialize();

// リスナー設定*前*に初期状態を記録
final initialState = container.read(appStateProvider);
recorder.record(AppSnap.fromAppState(initialState));

// 後続の状態変化をリッスン
container.listen<AppState>(appStateProvider, (prev, next) {
  // 関連するすべての状態変化を自動的に記録
  recorder.record(AppSnap.fromAppState(next));
});

キーポイント:

TraceRecorder<AppSnap>は、スナップショットの型AppSnapで型指定されます。

initialize()は記録プロセスを開始します（内部のトレースをクリアします）。
リスナーを設定する前に、初期状態を手動で記録します。
状態管理リスナー（ここではRiverpodのcontainer.listen）は、元のAppStateが変更されるたびに自動的にrecorder.record()を呼び出し、状態遷移のフローをキャプチャします。

 ステップ 3: プロポジションの定義 (state と event)次に、基本的な構成要素である原子プロポジション（Atomic Proposition）を定義します。これらはAppSnapに関する単純な真偽（True/False）の表明です。temporal_logic_coreのヘルパー関数を使用します：
import 'package:temporal_logic_core/temporal_logic_core.dart';

// ある期間継続する状態を表す条件には `state` を使用します。
final loading = state<AppSnap>((s) => s.isLoading, name: 'loading');
final home = state<AppSnap>((s) => s.isOnHomeScreen, name: 'home');
final error = state<AppSnap>((s) => s.hasError, name: 'error');

// 特定の時点でのイベント発生（しばしばトリガーとなる）を示す条件には `event` を使用します。
final loginClicked = event<AppSnap>((s) => s.loginClicked, name: 'loginClicked');

キーポイント:

state<T>は、アプリケーションが特定の状態にあることを表すプロパティ（例：isLoadingがtrueである）に使用されます。

event<T>は、瞬間的な出来事やトリガー（例：loginClickedがtrueである）をマークするために使用されます。この区別は、時相演算子が状態シーケンスをどのように解釈するかにおいて重要です。

 ステップ 4: Temporal Formula (LTL) の記述ここで、時間経過に伴う期待される振る舞いをTemporal Logicの式（Formula）として記述します。例えば、次のプロパティを検証したいとしましょう：「ログインボタンがクリックされた後は常に、次の状態でアプリはローディング中であり、かつ、アプリはいつかホーム画面に到達しなければならず、かつ、エラー状態には決してなってはならない。」
LTLの記法では、これは次のように表現できます：G(loginClicked -> (X loading && F home && G !error))
Dartパッケージのビルダー構文を使用して、これをコードで記述する方法は次のとおりです：
// LTL式: G(loginClicked -> (X loading && F home && G !error))
// 意味: 常に (G)、もし loginClicked イベントが発生したならば (->):
//  - 次 (X) の状態で loading が true であり、かつ (&&)
//  - いつか (F) home が true になり、かつ (&&)
//  - 常に (G) error は true ではない (!)。
final formula = always( // G(...)
  loginClicked.implies( // ->
    next(loading) // X loading
    .and(eventually(home)) // && F home
    .and(always(error.not())) // && G !error
  )
);

キーポイント:
論理演算子（implies、and、not）と時相演算子（always、next、eventually）を使用してプロポジションを組み合わせます。
ビルダー構文（.implies()、.and()、.not()、always(...)、next(...)、eventually(...)）により、式を読みやすく構築できます。

 ステップ 5: テストの実行と検証最後に、これらすべてをflutter_testのウィジェットテスト内で組み合わせます：
testWidgets('Successful login flow satisfies LTL formula', (tester) async {
  // 1. セットアップ: Recorder, ProviderContainer (上記参照)
  final recorder = TraceRecorder<AppSnap>();
  final container = ProviderContainer();
  addTearDown(container.dispose);
  recorder.initialize();

  // 2. 記録設定: 初期状態 + リスナー (上記参照)
  final initialState = container.read(appStateProvider);
  recorder.record(AppSnap.fromAppState(initialState));
  container.listen<AppState>(appStateProvider, (prev, next) {
    recorder.record(AppSnap.fromAppState(next));
  });

  // 3. UIセットアップ
  await tester.pumpWidget(
    UncontrolledProviderScope(container: container, child: const MyApp()),
  );
  await tester.pumpAndSettle();

  // 4. ユーザーインタラクションのシミュレーション
  await tester.enterText(find.byKey(const Key('email')), 'valid@email.com');
  await tester.enterText(find.byKey(const Key('password')), 'password');

  // *** 重要: 'クリック'イベントを手動で記録 ***
  // タップアクション直前の状態を取得
  final currentStateBeforeClick = container.read(appStateProvider);
  // イベント発生をマークした特別なスナップショットを記録
  recorder.record(AppSnap.fromAppState(currentStateBeforeClick, loginClicked: true));

  // タップアクションを実行 (これにより状態変化がトリガーされ、リスナーによって記録される)
  await tester.tap(find.byKey(const Key('login')));

  // 非同期操作 (ネットワーク呼び出しなど) とそれに続く状態変化が完了するのを待つ
  await tester.pumpAndSettle();

  // 5. プロポジションの定義 (上記参照)
  final loading = state<AppSnap>((s) => s.isLoading, name: 'loading');
  final home = state<AppSnap>((s) => s.isOnHomeScreen, name: 'home');
  final error = state<AppSnap>((s) => s.hasError, name: 'error');
  final loginClicked = event<AppSnap>((s) => s.loginClicked, name: 'loginClicked');

  // 6. LTL式の定義 (上記参照)
  // G(loginClicked -> (X loading && F home && G !error))
  // 意味: 常に (G)、もし loginClicked イベントが発生したならば (->):
  //  - 次 (X) の状態で loading が true であり、かつ (&&)
  //  - いつか (F) home が true になり、かつ (&&)
  //  - 常に (G) error は true ではない (!)。
  final formula = always( // G(...)
    loginClicked.implies( // ->
      next(loading) // X loading
      .and(eventually(home)) // && F home
      .and(always(error.not())) // && G !error
    )
  );

  // 7. 検証
  final trace = recorder.trace; // 記録された状態シーケンスを取得

  // temporal_logic_flutter のカスタムマッチャーを使用して検証
  expect(trace, satisfiesLtl(formula));

  // デバッグ用にトレースの内容を出力することも可能:
  // print(trace.events.map((e) => '${e.timestamp}: ${e.value}').join('
'));
});

キーポイント:

手動イベント記録: tester.tapの直前にloginClickedイベントを手動で記録することが重要です。これにより、LTL式のnext(loading)部分が正しく評価されます。後続の状態変化（loading状態への遷移、最終的なhome状態への遷移など）は、状態リスナーによって自動的に記録されます。

pumpAndSettle: 非同期のログインプロセスが完了し、関連するすべての状態変化が記録されるのを待ちます。

satisfiesLtl マッチャー: 記録されたtraceが指定されたLTL式を満たすかどうかを検証します。
この詳細な例は、主要なコンポーネント（AppSnap, TraceRecorder, プロポジション, LTL式, マッチャー）が連携し、Flutterアプリケーションにおける複雑な時間依存の振る舞いを形式的に検証する方法を示しています。

 5. 導入するメリットは？新しいテストアプローチを導入するには、それに見合うメリットが必要です。では、なぜFlutterのテストワークフローにTemporal Logicを組み込むことを検討すべきなのでしょうか？そのメリットは、単にテストケースが増えるというだけではありません：

明確な仕様: LTLやMTLの式を書くという行為自体が、時間経過に伴う意図された振る舞いについて正確に考えることを促します。「いつか（Eventually）」なのか「次の状態（Next）」なのか？「3秒以内」に起こる必要があるのか、それとも後でいつでも良いのか？これらの式は、明確で実行可能な仕様として機能し、要件の曖昧さを減らし、開発とテストの認識を一致させます。

潜在的なバグの発見: これこそがTemporal Logicの核心的な強みです。従来の方法では見つけるのが困難なバグを検出することに優れています：

順序の問題: State BがState Aの前に現れてはいけないのに現れてしまった、といった問題。非同期操作が、UIが完了したと想定した後に完了してしまう（競合状態）。

タイミングの失敗: ローディングインジケーターが表示されるのが速すぎたり遅すぎたりする。アニメーションがカクついたり、想定以上に時間がかかったりする。タイムアウト機構が正しくトリガーされない。

一時的な状態エラー: 複雑な遷移の途中で、UIが一瞬だけ不正な状態になってしまう。LTL/MTLは状態シーケンスの全体を評価するため、これらの一時的な不整合を捉えることができます。


信頼性の向上: 重要なユーザーフロー（ログイン、チェックアウト、データ送信など）における状態遷移の順序とタイミングを形式的に検証することにより、それらの正確性と信頼性に対する確信が大幅に向上します。単に開始点と終了点をチェックするだけでなく、プロセス全体の流れを検証していることになります。

的を絞った表現力豊かなテスト: 時間的な振る舞いを間接的に推測するために、複数のpump呼び出し、遅延 (Future.delayed)、手動での状態チェックなどを組み合わせた複雑なflutter_testコードを書く代わりに、Temporal Logicは専用の演算子（always, eventuallyTimedなど）とマッチャー（satisfiesLtl）を提供し、これらの性質を直接的に表現・検証します。これにより、テストは関心のある特定の時間的側面に、より焦点を絞ったものになります。
多少の学習コストはかかりますが、Temporal Logicテストを導入することで、動的なユーザーインターフェースにおける時間という要素がもたらす複雑さに体系的に対処し、より堅牢なアプリケーションを構築することにつながる可能性があります。

 6. 始め方ご自身のFlutterアプリでTemporal Logicを用いたテストを試してみませんか？始めるための手順は以下の通りです：
リポジトリの探索:
ここで説明したパッケージや例を含む完全なソースコードはGitHubで公開されています：https://github.com/CAPHTECH/temporal_logic
リポジトリをクローンして、ローカルでコードを探索します：
git clone https://github.com/CAPHTECH/temporal_logic.git
cd temporal_logic
依存関係の追加:
必要なパッケージをpubspec.yamlに追加します。通常はtemporal_logic_flutter（内部で_coreを取り込む）が必要になります。時間制約付きの検証を行いたい場合はtemporal_logic_mtlも追加します。
dependencies:
  flutter:
    sdk: flutter
  # 状態管理など、他の必要な依存関係を追加 (例: flutter_riverpod)

dev_dependencies:
  flutter_test:
    sdk: flutter
  temporal_logic_flutter: # 最新バージョンは pub.dev またはリポジトリで確認してください
  # temporal_logic_mtl: # 時間制約付き演算子を使用する場合に追加
  # temporal_logic_core: # 通常は _flutter または _mtl 経由で含まれるため、明示的な追加は不要
プロジェクトディレクトリでflutter pub getを実行します。
例の実行:
実践的な使い方を理解する最良の方法は、リポジトリのexamples/ディレクトリにある例（login_flow_ltl、snackbar_mtlなど）を実行してみることです。
例のディレクトリ（例：cd examples/login_flow_ltl）に移動し、テストを実行します：
# FVM (Flutter Version Management) を使用している場合 (一貫性のために推奨)
# これにより、プロジェクトで定義された特定のFlutterバージョンが使用されます。
fvm flutter test

# または、グローバルにインストールされたFlutter SDKを使用している場合
flutter test
各例のtest/widget_test.dartファイルを調べて、AppSnap、TraceRecorder、LTL/MTL式、マッチャーがどのように使用されているかを確認します。
簡単なものから始める:
まず、ご自身のアプリケーションで、比較的単純でありながら時間依存の側面を持つフローを特定します。
そのフローに関連する最小限のAppSnapクラスを定義します。

TraceRecorderと状態リスナーを設定します。
基本的なLTL式（例：always、eventually、nextを使用）を記述し、satisfiesLtlマッチャーで検証します。

 7. 結論と次のステップFlutterアプリケーションにおける動的で時間経過に依存する側面をテストすることは、独特の難しさがあります。従来のテスト手法では、処理の順序、タイミング、そして一時的な状態の正当性を検証するには不十分な場合があります。Temporal Logicは、時間経過に伴う特性について形式的に推論する能力を備えており、これまでのテスト手法を補完する強力なアプローチとなります。
temporal_logic_flutterスイートは、このアプローチを既存のテストワークフローに統合するためのツール（TraceRecorder、LTL/MTL式ビルダー、flutter_testマッチャー）を提供します。正確な時間的仕様を定義し、それらを実行トレースに対して検証することにより、従来のテストでは見逃しがちだった潜在的なバグを捉え、複雑なユーザーフローに対する信頼性を高め、より堅牢なFlutterアプリケーションを構築できます。
次のステップ：

試してみる： リポジトリ（https://github.com/CAPHTECH/temporal_logic）をクローンし、例を実行し、ご自身のアプリの振る舞いに対するTemporal Formulaを書いて実験してみてください。

フィードバックする： 問題点や改善のアイデアがあれば、GitHubリポジトリでIssueを作成してください。

貢献する： ドキュメントの改善、例の追加、機能強化、バグ修正など、どのような貢献も歓迎します。
Flutterテストの可能性を共に押し広げ、見た目が美しく高性能であるだけでなく、時間的な側面においても正当性が検証されたアプリケーションを構築していきましょう。
合同会社CAPH TECHPublication
合同会社CAPH TECHではFlutterアプリ開発を行っています。また、Flutterの技術顧問として開発サポートや若手の育成を担当しています。
Widgetテストを超えて: LTL/MTLでFlutterのタイミング＆順序バグを捉える

1. 導入: Flutterテストにおける「時間」という挑戦

2. Temporal Logicとは？ (シンプルに！)

Linear Temporal Logic (LTL): 「いつ」の論理

Metric Temporal Logic (MTL): 「どのくらい」を追加する

3. `temporal_logic_flutter` スイートの紹介

4. 主要概念の実践: ログインフローの検証

ステップ 1: 状態スナップショットの定義 (`AppSnap`)

ステップ 2: トレースの記録 (`TraceRecorder`)

ステップ 3: プロポジションの定義 (`state` と `event`)

ステップ 4: Temporal Formula (LTL) の記述

ステップ 5: テストの実行と検証

5. 導入するメリットは？

6. 始め方

7. 結論と次のステップ

Discussion
