--- title: modality-ts - フロントエンドを様相論理でテストする tags: author: [ゆにねこ](https://image.docswell.com/user/9031733) site: [Docswell](https://www.docswell.com/) thumbnail: https://bcdn.docswell.com/page/GJWG88G172.jpg?width=480 description: modality-ts - フロントエンドを様相論理でテストする by ゆにねこ published: June 13, 26 canonical: https://image.docswell.com/s/9031733/ZDMW3G-modality-ts --- # Page. 1 ![Page Image](https://bcdn.docswell.com/page/GJWG88G172.jpg) modality-ts フロントエンドを様相論理でテストする ゆにねこ X @harineko_univ / GitHub @harineko0 # Page. 2 ![Page Image](https://bcdn.docswell.com/page/4EZL88LX73.jpg) 自己紹介 - ゆにねこ 2 # Page. 3 ![Page Image](https://bcdn.docswell.com/page/Y76WPPWP7V.jpg) フロントエンドをテストしてますか ? 3 # Page. 4 ![Page Image](https://bcdn.docswell.com/page/G75MKKMP74.jpg) 4 # Page. 5 ![Page Image](https://bcdn.docswell.com/page/9J29WW9ZER.jpg) Pain ● Unit testing は不十分 ● E2E (Playwright) の実装保守コストが高い ● Codex Browser Use は非決定的 5 # Page. 6 ![Page Image](https://bcdn.docswell.com/page/DEY4LL4NJM.jpg) 比較的 バックエンドのテストは容易 6 # Page. 7 ![Page Image](https://bcdn.docswell.com/page/VJNY44YV78.jpg) → 状態 (DB) と挙動 (API) が別だから (State モナド) 7 # Page. 8 ![Page Image](https://bcdn.docswell.com/page/YE9PQQPVJ3.jpg) # Page. 9 ![Page Image](https://bcdn.docswell.com/page/GE8DGGD4ED.jpg) golden test, AI, 目視 ? # Page. 10 ![Page Image](https://bcdn.docswell.com/page/LELMGGMV7R.jpg) 10 # Page. 11 ![Page Image](https://bcdn.docswell.com/page/4JMYQQYNJW.jpg) 状態を外に出したい Haskell Redux のように 11 # Page. 12 ![Page Image](https://bcdn.docswell.com/page/PJR9889479.jpg) 様相論理 12 # Page. 13 ![Page Image](https://bcdn.docswell.com/page/PEXQ88QZJX.jpg) 13 # Page. 14 ![Page Image](https://bcdn.docswell.com/page/3EK9KK9VED.jpg) 14 # Page. 15 ![Page Image](https://bcdn.docswell.com/page/L73WZZ9Q75.jpg) 15 # Page. 16 ![Page Image](https://bcdn.docswell.com/page/87DKRRGWJG.jpg) 16 # Page. 17 ![Page Image](https://bcdn.docswell.com/page/VJPKWW3XE8.jpg) LTL / CTL のソフトウェアテスト応用 Linear Temporal Logic Computation Tree Logic 17 # Page. 18 ![Page Image](https://bcdn.docswell.com/page/2EVV8843EQ.jpg) 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 # Page. 19 ![Page Image](https://bcdn.docswell.com/page/57GL551YEL.jpg) Model checking the convergence property of BGP networks https://www.jsoftware.us/vol9/jsw0906-34.pdf 19 # Page. 20 ![Page Image](https://bcdn.docswell.com/page/4EQYZZD6JP.jpg) フロントエンドへの応用 20 # Page. 21 ![Page Image](https://bcdn.docswell.com/page/KJ4W33ZM71.jpg) https://github.com/antithesishq/bombadil 21 # Page. 22 ![Page Image](https://bcdn.docswell.com/page/LE1Y11RY7G.jpg) https://github.com/antithesishq/bombadil 22 # Page. 23 ![Page Image](https://bcdn.docswell.com/page/GEWG8811J2.jpg) 実 DOM のテストしかない PBT 23 # Page. 24 ![Page Image](https://bcdn.docswell.com/page/47ZL88PXJ3.jpg) 外に出した状態を検証したい useState() atom(0) useSWR() 検査式 e.g. 重複して Submit できない 24 # Page. 25 ![Page Image](https://bcdn.docswell.com/page/YJ6WPPMPJV.jpg) modality-ts React を有限状態遷移に変換し, LTL で検証する 25 # Page. 26 ![Page Image](https://bcdn.docswell.com/page/GJ5MKKZPJ4.jpg) https://www.npmjs.com/package/modality-ts 26 # Page. 27 ![Page Image](https://bcdn.docswell.com/page/LE3WZZ96E5.jpg) Architecture App.tsx TypeScript AST 中間表現 検査式で検証 app.model.ts model.json app.props.mjs 27 # Page. 28 ![Page Image](https://bcdn.docswell.com/page/8EDKRRGM7G.jpg) Architecture App.tsx TypeScript AST 中間表現 検査式で検証 app.model.ts model.json app.props.mjs 28 # Page. 29 ![Page Image](https://bcdn.docswell.com/page/V7PKWW3QJ8.jpg) Architecture App.tsx TypeScript AST 中間表現 検査式で検証 app.model.ts model.json app.props.mjs 29 # Page. 30 ![Page Image](https://bcdn.docswell.com/page/2JVV884PJQ.jpg) Limitation 下記は未対応 (今後実装) ● useState, jotai, SWR 以外の状態管理 ● モデル化されていない外部サービス ● モデル化されていない並行処理、タイマー、ネットワーク競合 30 # Page. 31 ![Page Image](https://bcdn.docswell.com/page/5EGL551QJL.jpg) DEMO 31 # Page. 32 ![Page Image](https://bcdn.docswell.com/page/4JQYZZDW7P.jpg) Thank you 32