自動テストに限界を感じた私がなぜ形式手法に魅了されたのか - 若くない何かの悩み

長らく自動テストとテスト容易設計を生業としてきましたが、最近は色々な限界を感じて形式手法に取り組んでいます。 この記事では、既存の自動テストのどこに限界を感じてなぜ形式手法が必要なのかの私見を説明します。なお、私もまだ完全理解には程遠いため間違いがあるかもしれません。ご指摘やご意見はぜひ Kuniwak までいただけると嬉しいです。 著者について プログラマです。開発プロセスをよくするための自発的な自動テストを支援する仕事をしています（経歴）。ここ一年は R&D 的な位置付けで形式手法もやっています。 自動テストの限界 自動テストとは 私がここ数年悩んでいたことは、iOS や Web アプリなどのモデル層のバグを従来の自動テストで見つけられないことでした。ただ、いきなりこの話で始めると理解しづらいと思うので簡単な例から出発します。 この記事でいう自動テストとは以下のようにテスト対象を実際に

[devorgachem]

書きました / 形式手法を学びたければ PRINCIPIA さんのイベントがオススメです https://principia.connpass.com/event/177935/

[raitu]

たしかFeliCaは形式手法で作ってたよな/ ipaが形式手法導入事例まとめ資料作ってた https://www.ipa.go.jp/files/000005473.pdf

[kirakking]

それで工業面で使えるのかと思う人向けに: Isabelle/HOLだと8700行程のOSカーネル(seL4)の正しさの証明も出来ているよ。 https://m-hiyama-memo.hatenablog.jp/entry/20170811/1502431494　http://isw3.naist.jp/IS/Curriculum/18/Colloquium/colloquium-a/180605.pdf

[kwhrtsk]

AWSがDynamoやS3の検証に使ってたのはTLA+だっけ。

[n314]

15年くらい前に大学でやったけど、それっきりだな。実際に業務で使うための最初の一歩が全然分からない…。

[taka_sek]

テスト手法と形式手法の間をステップバイステップで丁寧に繋いでくれてる。よい。

[golden-lucky]

「従来のコードでさえ正しく書けないのに、より抽象度の高い論理式やモデルを最初から正しく書けるはずがない」からの「数理論理学の学習や基礎理論への理解がとても重要」

[t-tanaka]

自動テストについて，「限界があるからやらない」は間違っている。まずは限界までやってみるべき。その上で，カバーできない範囲のことを考える。

[ytakano]

大学の講義でアセンブラとマルチスレッドプログラミングと形式手法を組み合わせた簡単な課題を出してみたけれど、できる学生はかなり限られていた。分野を広くまたぐ必要があってなかなか難しい。

[SWIMATH2]

形式手法にいたるまでの過程の嬉しさと難しさがわかりやすくて良い

[tick2tack]

後半理解できてないが形式手法はこういう場面で有用だよということを知れてよかった。

[aprifield]

“なお上記のアプリについては、今回紹介した定理証明支援系とは別の形式手法である「モデル検査5」を試みました（詳細）。モデル検査は並列システムの網羅的な検証を得意としていて、私の悩みを解決できる有力な手

[misshiki]

“テストケースの増加につれ従来の自動テストに限界が訪れる 現実の設計で頻出する状態機械の合成はこの限界を超えてくる これに対応できる手段が形式手法である”

[syukit]

これを実際にできる気がしないw

[nihonbuson]

とても良い内容！「自動テストの限界」というより「テスト設計の限界」も示唆していて、それに対して勘所という名の経験則を使うのとは全く別のアプローチを試みているのが大変良い。

[ledsun]

テストに形式手法。なるほど

[mkataigi]

どっちが有用っていうより、使い分けようって話かなぁ。注釈３に書いてあることだけど、形式手法だと「アルゴリズム」の証明はできても、「コード」の検証はできない気がする。

[programmablekinoko]

抜き取り検査から定理証明へと言う感じ

[miya-jan]

“従来のコードでさえ正しく書けないのに、より抽象度の高い論理式やモデルを最初から正しく書けるはずがないのです”

[raimon49]

Parameterized TestやProperty-based Testingといった抽象化の先にあるもの。

[otihateten3510]

プログラム検証の話でしょ？数学的に正しさを証明するみたいな。大学でやってたけど使い所としてはカーネルや衛星や医療、金融あたりに限られるよね。

[Rinta]

“どんな自然数 x であっても x + 0 = 0 を満たす” これは直しておこう。有益な記事お疲れ様。

[t-murachi]

humm...

[skypenguins]

やっぱ数理論理学って大事なんだな〜

[zou3dazou]

"単条件のテストケース追加 → Parameterized Test → 同値分割・境界値分析 → (入出力の具体性の壁) → Property-based Testing → (網羅性の壁) → 可能なら入力空間の制限 → (扱える入力空間の大きさの壁) → 形式手法"

[mickn]

[

[snowcrush]

"したがって形式手法においても自分の記述したモデルや論理式が自分の意図通りになっているか確かめる作業は避けて通れません" テストが複雑になればなるほどテストプログラムそのものの正当性に確信が持てなくなる

[tanority]

テスト

[Phenomenon]

これ系って滅んでてスマートコントラクト回りで使われてるだけかと思ってた

[jagaimojanaizo]

[[テスト]‌][プログラミング]

[ngmy]

林晋先生かと思ったら違った。 http://www.shayashi.jp/myfailures.pdf

[akiramaz]

すごい