なぜ人々は形式手法を使わないのか？

この質問をSoftware Engineering Stack Exchangeで見かけました。形式手法の広範な採用を妨げている障壁は何でしょうか？質問は意見ベースとして閉じられ、ほとんどの回答は「高すぎる!!!」とか「ウェブサイトは飛行機じゃない!!!」といったものでした。これらはある程度正しいですが、あまり多くを説明していません。この記事では、形式手法の歴史的な全体像、なぜ実際にはそれほど使われていないのか、そしてそれらが使われるようにするために何をしているのかを説明します。 始める前に、いくつかの用語を定義する必要があります。形式手法のコミュニティというよりは、草原をさまよう小さな集団がいくつかあるだけです。そのため、異なるグループが用語を異なる方法で使用します。非常に大まかに言うと、FMには2つの領域があります。形式仕様は、正確で曖昧さのない仕様をどのように書くかの研究であり、形式検証は、物事が正しいことをどのように証明するかの研究です。しかし、「物事」にはコードと抽象的なシステムの双方が含まれます。それらを指定するためには別々の手段を使うだけでなく、検証するためにもしばしば異なる手段を使います。 さらに混乱を招くことに、誰かが形式仕様を行っていると言う場合、通常は仕様と検証の両方を意味し、形式検証を行っていると言う場合は、通常は仕様と検証の両方を意味します。明確にするために、検証をコード検証（CV）と設計検証（DV）に分け、同様に仕様をCSとDSに分けます。これらは、より広いFMの世界で使われる用語ではありません。まずCSとCVについて話し、次にDSとDVに移ります。 さらに、仕様の一部のみを検証する部分検証や、仕様全体を検証する完全検証を行うこともできます。これは、「クラッシュしない、または間違ったパスワードを受け付けない」という証明と、「クラッシュしない、または間違ったパスワードを受け付けない、そして間違ったパスワードを3回入力したらアカウントをロックする」という証明との違いになり得ます。この歴史のほとんどは、完全検証を行っていることを前提としています。 形式化するソフトウェアの種類も明確にする必要があります。ほとんどの人は、医療機器や航空機のような高信頼性ソフトウェアと、それ以外のソフトウェアを暗黙的に分けています。人々は、前者では形式手法が広く使われており、後者では不要だと想定しています。これは、もしあれば、楽観的すぎます。高信頼性ソフトウェアのほとんどの人は形式手法を使用していません。代わりに「通常の」ソフトウェアに焦点を当てます。 最後に、免責事項です。私は歴史家ではなく、注意を払ったつもりですが、間違いがある可能性があります。また、私は形式仕様（DSとDV）を専門としているため、コード検証について述べることには間違いがある可能性が高いです。もし何か間違っている点を見つけたら、私にメールしてください。修正します。 形式コーディング 仕様の取得 コードが正しいことを証明する前に、「正しい」とは何かを知る必要があります。これは、コードが何をすべきかの仕様、またはスペックを持つことを意味します。そこでは、特定の出力がスペックに従っているかどうかを曖昧さなく言うことができます。「ソートされている」というリストの単なる記述は不明瞭です。何をソートしているのか、どの基準を使っているのか、あるいは「ソート」で何を意味するのかさえわかりません。代わりに、「整数のリストlは、任意の2つのインデックスiとjに対して、i < jならばl[i] <= l[j]である場合、昇順にソートされている」と言うかもしれません。 コードスペックは3つの主要なキャンプに分類されます。 最初のキャンプは、コードとは独立したステートメントとしてそれらを記述することです。ソート関数を書き、別のファイルに「これはソートされたリストを返す」という定理を書きます。これはスペックの最も古い形態であり、IsabelleとACL2が現在も行っている方法です。 2番目のキャンプは、プリ/ポスト条件、アサーション、不変条件の形でスペックをコードに埋め込むことです。関数に「戻り値はソートされたリストである」というポスト条件を追加するかもしれません。アサーションベースのスペックは、元々Hoare Logicとして形式化され、1970年代初頭にEuclidというプログラミング言語に初めて統合されました。このスタイルはDesign by Contractとも呼ばれ、産業用検証で最も人気のある形態です。 最後に、型システムがあります。Curry-Howard対応により、任意の数学的定理や証明は依存型としてエンコードできます。私たちは「ソートされたリスト」の型を定義し、私たちの関数が[Int] -> Sorted [Int]という型シグネチャを持つと宣言します。これらすべての例は「Let’s Prove Leftpad」で見ることができます。HOL4とIsabelleは「独立した定理」スペックの良い例であり、SPARKとDafnyは「埋め込みアサーション」スペックを持ち、CoqとAgdaは「依存型」スペックを持っています。 少し目を細めて見ると、これら3つのコードスペックの形式は、自動的な正しさチェックの3つの主要な領域、つまりテスト、契約、型に対応しているように見えます。これは偶然ではありません。正しさはスペクトラムであり、形式検証はそのスペクトラムの一方の極端です。検証の厳密さ（と労力）を減らすにつれて、探索される状態空間を制限したり、弱い型を使用したり、検証を実行時にプッシュしたりするなど、より単純で狭いチェックが得られます。したがって、全仕様のあらゆる手段は部分仕様の手段となり、その逆もまた然りです。Cleanroomを形式検証技術と見なす人もいますが、それは主にコードレビューを人間が可能なレベルをはるかに超えてプッシュすることによって機能します。 「正しいスペックとは何か？」 検証は、コードがそのスペックに一致することを証明します。これは、「正しいスペックをどのように知るのか？」という疑問を提起します。正しいスペックを見つけることは、形式手法における最大の課題の1つです。また、最もよく提起される異議の1つでもありますが、懐疑論者がそれを意味する方法は、提唱者がそれを考える方法と正確には同じではありません。 部外者が「正しいスペックをどうやって手に入れるんだ？」と言うとき、彼らは通常、検証（validation）を考えています。つまり、スペックが実際にクライアントが望むことをしていることを示すことです。リストをソートするコードを形式的に証明しても、顧客が実際にUber For Soups™を望んでいる場合、あなたは単に時間を無駄にしただけです。人々は、迅速なイテレーションと短いフィードバックサイクルによってのみ、要件を実際に検証できると主張します。 コードを検証してもコードが検証されるわけではないというのは本当です。しかし、この議論には2つの問題があります。最初の問題は、それがFMの価値を完全に排除するのではなく、単に遅らせるだけであるということです。迅速なイテレーションを行った後、おそらく顧客が何を望んでいるかについてのアイデアがあるでしょう。それからコードの検証を開始します。2番目の問題は、顧客が正確に何を望んでいるかはわからないものの、彼らが望まないであろういくつかのことを仮定できるということです。彼らはソフトウェアがランダムにクラッシュすることを望んでいません。彼らはセキュリティホールを望んでいません。誰もがこの重要性を認識しています。結局のところ、イテレーション中に単体テストをスキップすべきだと言う人はいません。したがって、少なくとも、バージョン管理システムがユーザーの本の章をランダムに削除しないことを証明してください。 正しいスペックを見つける問題は、より根本的です。私たちはしばしば、スペックが何であるべきかを知りません。私たちは、数学的な言葉ではなく、人間の言葉で要件を考えます。もし私が「これは公園と鳥を区別すべきだ」と言ったら、何を言っているのでしょうか？人間には、公園と鳥の絵をいくつか見せることで説明できますが、それは単なる具体的な例であり、公園と鳥を区別するという考えを捉えていません。それを形式的なスペックに実際に翻訳するには、人間の概念を形式化できる必要があります。そして、それは深刻な課題です。 誤解しないでください。適切なスペックを見つけることは可能です。専門家は常にそれを行っています。しかし、適切なスペックを書くことは、コーディングスキルを開発する必要があったのと同じように、開発する必要のあるスキルです。 そのため、コード検証における最近の成功の多くは、私たちが望むことと、私たちが望むことを表現できることとの間に明らかなマッピングがあるものです。例えば、CompCertは形式的に検証されたCコンパイラです。そこでのスペックは「これは決して誤コンパイルしない」ということです。そして、これらは実際の検証部分ではありません。仕様が得られたら、コードが仕様に一致することを証明する必要があります。 仕様の証明 私たちが目にする最も初期のコード検証手段は、Dijkstraスタイルの「それが真実である理由を一生懸命考える」という方法です。これは基本的にALGOLが助けるために設計されたものです。