modality-ts - フロントエンドを様相論理でテストする

modality-ts フロントエンドを様相論理でテストする ゆにねこ X @harineko_univ / GitHub @harineko0

自己紹介 - ゆにねこ 2

フロントエンドをテストしてますか ? 3

4

Pain ● Unit testing は不十分 ● E2E (Playwright) の実装保守コストが高い ● Codex Browser Use は非決定的 5

比較的 バックエンドのテストは容易 6

→ 状態 (DB) と挙動 (API) が別だから (State モナド) 7

golden test, AI, 目視 ?

10

状態を外に出したい Haskell Redux のように 11

様相論理 12

13

14

15

16

LTL / CTL のソフトウェアテスト応用 Linear Temporal Logic Computation Tree Logic 17

Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 https://assets.amazon.science/07/6c/81bfc2c243249a8b8b65cc2135e4/using-lightweight-formal-method s-to-validate-a-key-value-storage-node-in-amazon-s3.pdf 18

• https://assets.amazon.science/07/6c/81bfc2c243249a8b8b65cc2135e4/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3.pdf

Model checking the convergence property of BGP networks https://www.jsoftware.us/vol9/jsw0906-34.pdf 19

• https://www.jsoftware.us/vol9/jsw0906-34.pdf

フロントエンドへの応用 20

https://github.com/antithesishq/bombadil 21

• https://github.com/antithesishq/bombadil

https://github.com/antithesishq/bombadil 22

• https://github.com/antithesishq/bombadil

実 DOM のテストしかない PBT 23

外に出した状態を検証したい useState() atom(0) useSWR() 検査式 e.g. 重複して Submit できない 24

modality-ts React を有限状態遷移に変換し, LTL で検証する 25

https://www.npmjs.com/package/modality-ts 26

• https://www.npmjs.com/package/modality-ts

Architecture App.tsx TypeScript AST 中間表現 検査式で検証 app.model.ts model.json app.props.mjs 27

Architecture App.tsx TypeScript AST 中間表現 検査式で検証 app.model.ts model.json app.props.mjs 28

Architecture App.tsx TypeScript AST 中間表現 検査式で検証 app.model.ts model.json app.props.mjs 29

Limitation 下記は未対応 (今後実装) ● useState, jotai, SWR 以外の状態管理 ● モデル化されていない外部サービス ● モデル化されていない並行処理、タイマー、ネットワーク競合 30

DEMO 31

Thank you 32