形式手法: 単なる良い工学実践なのか? (2024)
(brooker.co.za)- 大規模・分散・重要な低レベルシステムでは、形式手法は正確性のためだけの追加手順ではなく、時間とコストを削減する工学実践とみなすべき
- ソフトウェアは設計と実装が容易に混ざり合うため、遅い段階での設計修正はそのまま実装のやり直しや API 変更コストにつながる
- 実装前に動作とインターフェースを具体的に検討すれば、バグ密度や本番投入後の問題を減らし、より速く正しい設計にたどり着ける
- 急速に変化するユーザー要求や UI・ドキュメント・価格ロジックのように形式化しにくい領域では、全面的な事前形式設計の有効性は低くなりうる
- TLA+、P のようなツールは、設計段階で最適化と制約を検討し、正確性と性能のトレードオフを減らすためにも使える
良い工学実践としての形式手法
- 形式手法は、良いソフトウェアエンジニアリング実践の重要な一部である
- 特に大規模システム、分散システム、重要な低レベルシステムを扱うエンジニアにとって適用価値が高い
- 工学は最終的に時間とコストを最適化する活動である、という前提から出発する
- 性能、拡張性、持続可能性、効率性もあわせて考慮される
- 形式手法は安価でも容易でもなく、すべての開発方式にうまく合うわけでもないが、コストだけを増やすという直感は常に正しいわけではない
コストを下げる2つの経路
- 1つ目は手戻りの削減である
- ソフトウェアは他の工学分野と異なり、設計と構築が同時に進みやすい
- 設計が十分に進んでいなくても実装を始められる
- この可変性はソフトウェアの強みだが、設計の反復を実装の反復に変えてコストを増大させることがある
- 2つ目は変更コストの管理である
- API やシステムに顧客がつくと、変更ははるかに高価で困難になる
- Hyrum’s Law によれば、十分な数の API 利用者がいるとき、契約内容に関係なく観測可能なあらゆる挙動に誰かが依存するようになる
- API によってシステムの動作を隔離することはソフトウェアエンジニアリングの重要な考え方だが、利用者が実装詳細にまで依存しうるという限界は残る
- API の背後のシステムを完全に再実装することはできても、抽象化が変更コストそのものをなくすわけではない
- 形式的な設計作業は、手戻りコストを下げ、インターフェース変更をより早い時点で処理できるようにして、ソフトウェア構築の速度と効率を高めうる
形式設計が適しているシステム
- すべてのソフトウェアに同じ形で適用できるわけではない
- 急速に進化したり、形式化しにくいユーザー要求が多かったりするソフトウェアでは、事前設計の価値は弱まることがある
- UI、Web サイト、価格ロジックの実装などがこれにあたる
- こうした領域では継続的な手戻りが多く、事前設計コストが大きくなりうる
- アジャイルの基本的な考え方は、実装と要求収集を並行して進め、リリースまでの時間を短縮することである
- 要求収集が継続している場合でも、実装を完了できるようにする
- 多くの場合、この並行開発方式は最適であるか、あるいは前進を可能にする必須条件である
- 逆に、大規模・分散・低レベルシステムの多くの部分では、要求事項がよく理解されている
- 少なくとも十分に大きな静的要求事項の部分が存在する
- この場合、事前の形式設計は実装段階および本番投入後の手戻りとバグ密度を大幅に減らせる
- 要求事項が物理法則に近いほど設計と形式設計の価値は高くなり、ユーザーの意見に近いほどその価値は小さくなる
要求事項の文書化と形式化の限界
- ユーザー要求事項を明確に書き出すことは、形式的であれ非形式的であれ、非常に価値が高い
- 要求事項を書かなければ時間が浪費され、人々が互いに異なる方向へ動いて摩擦が生じうる
- すべての人間の要求事項を形式的に仕様化するのは、難しいか、経済的でないことがある
- UI の美的要件
- ドキュメントの可読性
- API 名の一貫性
- 形式的アプローチに対する意見の違いは、形式的アプローチとは何か、どのように価値を持つのかについての異なる考えからも生じる
- UML のようにコードを膨大な図式へ移し替える方式は、難しい問いを直接扱えないなら価値が低くなりうる
- 悪いやり方や悪いツールで行えば、価値ある作業でも役に立たなくなることがある
現場で有用な形式手法とツール
- 形式手法と自動推論は広い分野であり、多様なツールがある
- 大規模クラウドシステムの領域で有用だったツール群は次のとおり
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 は、軽量形式手法を見る出発点である
- 実装検証だけが唯一の目標ではない
- TLA+ や P のようなツールは、実装前に設計をより速く、より具体的に検討するうえで大きな価値がある
より速いソフトウェアを、より速く作る
- 2015年の How Amazon Web Services Uses Formal Methods 執筆時点では、焦点は主に正確性にあった
- 設計の安全性および活性の性質を検証すること
- 正しい設計により速く到達すること
- 内部ロック管理システムに TLA+ を使っていたチームの事例では、積極的な最適化を検証したという点が重要だった
- TLA+ のようなツールは、システムをより速く作れるようにするだけでなく、より高速なシステムを作れるようにもする
- 可能な最適化を素早く探索する
- 本当に重要な制約を見つける
- 提案した最適化が正しいことを確認する
- 多くの場合、形式手法はシステムが陥りがちな正確性と性能の難しいトレードオフを減らしてくれる
設計段階で使うツールの価値
- システム設計を考える助けになるツールを設計段階で使うと、ソフトウェア開発の速度を大きく高められる
- リスクを減らし、最初からより最適化されたシステムを作れるようにする
- 大規模で複雑なシステムを作るエンジニアにとって、形式手法は良い工学実践の一部である
1件のコメント
Hacker Newsのコメント
ソフトウェアの形式検証は、記事でも認めているように、ソフトウェアの種類と開発プロセスに大きく左右される
形式検証を使うには、ソフトウェアの振る舞いに関する形式的な要件が必要だが、ほとんどのプロジェクトや設計思想はこれに合わない。何を求めているのかもはっきりしない状態で開発と設計が同時に進むなら、形式手法は適用しにくい。ただし、小規模で安全性が重要なシステムのように、事前仕様に依存する領域では大きな恩恵を得られ、航空宇宙ソフトウェアがその代表例である
今では博士号や何年もの研究がなければ身につかない技術ではなく、基本的な高水準仕様を書くことも同じだ。モデルチェッカーを使えば、モデル化しているシステムについて何かを学ぶことになり、文書化や教育目的だけに使っても有用だ。形式手法の根本的な力は、最後まで考え抜かせる点にある。多くの開発者は、自分の頭、型チェッカー、少しのユニットテストだけで並行性アルゴリズムを実装できると信じているが、モデルチェッカーを走らせた後に設計や仮定の誤りを見つけると、謙虚にならざるを得ない。思ったより小さな分散システムは多く、状態空間は形式化してみる前の予想よりはるかに大きいことが多い
例えば、非常に厄介な状態機械にプロパティベーステストを付けて、どんな奇妙な入力でエンドポイントを呼び出しても、内部の状態機械が無効な遷移をしないよう確認した。周辺コードには形式仕様がないが、状態機械にはあったから可能で、従来のユニットテストでは絶対に見つけられなかった微妙なバグも見つけた
ただし形式手法の恩恵を得るには、プログラムの振る舞いをプログラム自体ではない別のものと比較する必要があり、その別のものも形式言語で書かれていなければならない。望ましい振る舞いを正確に理解する必要はあるが、ソフトウェア全体の振る舞いをすべて網羅する必要はない。自動化されたユニットテストも形式仕様であり、それを実行することは形式検証の方法だ。一般に言われる形式手法より弱い仕様と弱い検証にすぎず、概念的にも実務的にも明確な質的差があるわけではない。テストが適用可能なソフトウェアなら、より豊かな形式仕様の方法も適用できる可能性が高く、費用対効果はテストを学ぶように試行錯誤で身につけることになる
結局、「アジャイル」と呼ばれるためにどれだけ余分な金と時間を使うのかという問題だ。逆説的に、従来の要件定義フェーズが3つの方法の中で最も安く、変更コストが最も低い、テキスト1行を変える段階で顧客と素早く収束するため、本来のアジャイル精神にも最もよく合っている
それでも、すべてのケースを取りこぼしていないか、システム内に矛盾がないかを確認する恩恵は得られる
形式手法について、「ソフトウェアは大きく複雑で、正しく作るのが難しい。だから形式手法だ」という論理をよく見かける。
一方では、これが本当であってほしいとも思う。学問的に学ぶ方法に強いので個人的にも得だし、実務的にも、ソフトウェアが実際に複雑で失敗したときに原因を探し回るのはもどかしいからだ。だが、形式手法がその問題をどう解決するのかを説得力をもって示す例はほとんどない。この記事は、現代の「設計」の大半が時間の無駄だと指摘している点ではましだが、TLA が UML よりなぜ優れているのかは十分に説明していない。まるで、数か月あるいは数年を TLA に投資すれば悟りを得て、悟っていない人には説明できない形で有用だと分かる、という含みのように聞こえる。微積分やベイズ統計にもそういう面はあるので不可能な話ではないが、結局は「本当にそれほど有用なら、もっと多くの人が使っていて、利点は自然に明らかになっていたはずだ」というプロジェクトマネージャー的な判断に戻ってしまう。昔から存在しているのに広く定着していないなら、理由がある可能性が高い。
考えるのが難しい問題に出会うと、何らかの「方法」を使うことになる。通信プロトコルなら状態機械で説明するのがよく、TLA はそのニッチによりよく合っている。最近はそこまでの労力を正当化する問題は多くなかったが、そういう問題が出てきたときには非常に大きな価値がある。ドメイン特化言語も同様で、さまざまな問題を避けるには自分でパーサを書くより、パーサフレームワークを使う方がはるかによい。今ある手戻りの大半は、要件変更と、顧客が実際に何を望んでいるのか分からないまま「それではない」と言うことから来ている。依頼する側が自分たちの要求の含意を十分に考えていない面もあるが、よい判断を下すための知識が一か所に十分集まっていないことの方が大きい。
形式手法が大きな投資であることは間違いない。ただし一般的には定着していなくても、そのアイデアの一部は現代の型システムに取り込まれている。
受けた印象は、形式検証器の厳密さが、妥当な時間とメモリ内で終わらなければならないという理由だけでも設計の複雑さに上限を課す、ということだ。もしかすると、形式検証を求めることの本当の勝利は、「ソフトウェアは大きく複雑で、正しく作るのが難しい」という問題を、大きく複雑なプログラムを扱うのを面倒にすることで直す点にあるのかもしれない。
SAT や TLA の手法を使って入力空間を再現可能な形で素早く絞り込む、プロパティベーステストの後継を見てみたい。パースとコードカバレッジを通じて、関数に 12 を渡すことは 11 と別の分岐に進み得ないが、-1 や 2^17 < n < 2^32 のような値は異なる可能性がある、と推論できるべきだ。
いまだに大半のソフトウェアプロジェクトは失敗している。これは「市場の失敗」ではなく、単に「作ることに失敗している」に近い。
形式手法には大きく二つの流れがある。コード自体から分離され、通常はコードの仕様を推論する外在的手法と、コードの中に入り込み、コードをより直接的に推論する内在的手法だ。
歴史的には、型システムのような内在的手法は関数レベルでコードを推論し、Spin/P のような決定可能なモデル検査器などの外在的手法は、オートマトンのような形式主義で記述されたコードモデルを扱っていた。今は形式手法研究の黄金期だと思っており、型システムの発展や Verus のようなプロジェクトが推し進める内在的手法に比べ、外在的手法は次第に好まれなくなっている流れに見える。https://github.com/verus-lang/verus
Rust のようにフットプリントの大きい言語でこれがどう機能するのかという質問は見たことがあるが、よい答えはまだ見ていない。もっと読んでみたい。
内在的手法は別個の仕様を書いて保守しなくて済むため好まれる、という話に聞こえたが、実際にはそうではない。
軽量形式手法に触れている部分はよい。コードベースの横に proptest の戦略集を維持することは、手作業の単体テストを書くよりはるかに大きな投資ではないが、広いカバレッジと小さく理解しやすい失敗例のおかげで、はるかによい洞察を与えてくれる。
何より、このアプローチは一般的なソフトウェア開発の慣行にもよく合う。https://crates.io/crates/proptest
よいテストの書き方とそこに必要な労力はある程度分かっているが、LLM は私よりはるかに速く、よりよいテストを作れる。反復的で退屈な作業をしていると忍耐力が落ちる私より、むしろ手を抜かない可能性が高い。ソフトウェアエンジニアなら、反復的に感じる作業は自動化しようとする反射があるべきで、ドキュメント化も最近は生成することで、より頻繁に、より早い段階で行うようになる。LLM は形式検証の採用に小さな革命を起こすかもしれない。正しい仕様の生成は退屈である一方、動くコード・ドキュメント・ヒントといった十分な文脈があれば、LLM にとっては比較的簡単な作業かもしれない。仕様をすべて自分で直接書くのではなく、生成させたうえでざっと確認できるなら、はるかにやる気になれる。Rust を使うということは正確性を重視しているというシグナルでもあり、そのコンパイラは、形式手法なしでシステムがおそらく正しいことを証明するものに最も近いツールに近い。コンパイラも明示的な型もない言語に形式手法を後付けするより、はるかに容易である可能性が高い。
ソフトウェアの形式検証は、今でも極端なケースでない限り、価値が出るほど使うには難しすぎる。逆にハードウェアの形式検証は、使わない理由がないレベル
ずっと学ぼうとしているが、たいていのシステムでは「コンパイラを自分で書いた人」級の専門家でなければならない。たとえば varint のエンコーダ／デコーダを証明しようとしたところ、1〜2バイトはできたが、それ以上はできなかった。助けを求めると、コンパイラ内部でループを5回だけ展開する、といった、到底知りようのない内部詳細が原因だった。最近 Lean を学んでいて、気に入ってはいるが、こういう文書に出くわす：“Definitional equality includes η-equivalence…” といった具合。Lean をけなしたいわけではなく、むしろ選択肢の中では文書が良いほうに見える
形式手法は必ずしも複雑である必要はない。問題は、たいていの形式手法が、教授が関心を持っていた特定のテーマを示すための学術的演習のように設計されていることにある。TLA+ も論文を書くために設計された側に近い
軽量な形式手法の中で、広く知られてはいないが気に入っているものは、線形時相論理を使ったトレース検証: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
基本的にはイベントをログに記録するだけでよく、イベント駆動アーキテクチャでは事実上タダで得られることもある。そのうえで、実行トレースに
Always(Locked, Implies(Eventually(Unlocked)))のような述語を走らせればよい。過去のトレースにも適用でき、ストレステストやファジングと組み合わせて状態空間を探索することもできる。単純で強力、広く適用可能で、モデルなしに述語だけあればよい形式手法は、システムの振る舞いについて包括的な根拠を含意する。TLA や類似のシステムでは、実際のシステムではなく状態機械ではあるものの、その出力は LTL/CTL/TLA の性質がシステムのすべての振る舞い、つまりトレースやトレース木について成り立つという証明である
以前の議論は2024年6月にあった: https://news.ycombinator.com/item?id=40753989
15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - 2024年5月、コメント1件
遅すぎる。計画はすぐに化石化であり、どんな文書でもアジャイル法廷では不利な証拠として使われうる
形式手法について読んだ記事の大半は、コンサルタントの見込み客獲得のように感じる
それ自体は構わないが、社員や同僚に教育パッケージを買わせたり、自分を雇えば、悪い、さらには無責任なほど危険なプログラミング習慣を直してやる、という具合に形式手法による悟りに達したかのように振る舞われると不快だ。形式手法が、仕様から逸脱できない高品質なコードを実際に生成するようになったら、また話してほしい
形式仕様では通常、そこまでの詳細は指定せず、システムの一般的な振る舞いを指定する。そのため、1つの仕様が、微妙に異なる多くのプログラムに対応することが多い。コードが文書として不十分な理由もここにある。何が意図された選択で、何が偶然の選択なのか分からないからだ。コードは高水準の要求を説明するには具体的すぎる。逆に、仕様に対してプログラムを検証するほうが実現可能性は高い
現在の形式手法支持者の一部は、形式手法を使わない人を「怠け者」や「愚か者」と見なし、自分たちは「正しいことをしている」あるいは「複雑な言語を習得した」という理由で優位性を主張しようとする
もちろん全員ではなく、良い人たちも知っているが、一部は実のところ一芸だけの人に近い。ここ数年で学んだ、あるいは試した別の形式手法システムを尋ねると、「忙しすぎて」新しいものを学べないと言う。最近の、より使いやすい形式手法としては、Python 方言を使って疑似コードのように読める FizzBee、より簡単な構文を持つ Quint、C# ユーザーになじみのある構文の P がある。この記事の著者も、形式手法は自分の問題の半分しか解決しないと書いたことがある: https://brooker.co.za/blog/2022/06/02/formal.html
だが、そこで述べられている問題は、新しくもない PRISM がすでに解決している。Brooker が周囲を探したり学ぼうとしたりしていないだけだ