LLMはコードの正しさを証明できないが、証明のための定型作業は書ける
クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。
クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。…
cleanroom-correctness
6 posts
Cleanroom は 1KLOC あたり 0.1 defect を達成する。フル導入しなくてもそこに到達できる。
Cleanroom software engineering は defect rate を 100 倍に削減するが、フル導入には分離した test team と formal proof が必要。ここでは、overhead なしにその大半の benefit を得られる pragmatism なサブセットを紹介する。
Cleanroom software engineering は 1,000 行あたり 0.1 の defect を達成する。業界平均は 10 から 50 だ。問題は、フルの Cleanroom ではチームを author と verifier に分割し、すべての module の前に formal…
IBMのZero-Defect ProcessはKLOCあたり0.1 Bugを達成した。それでも業界は見捨てた。
IBMのCleanroom engineeringは業界平均より100倍優れたdefect rateを達成し、その後忘れ去られた。消えた理由は、それが機能したかどうかとは無関係だった。
IBMのCleanroom software engineering processは、千行あたり0.1のdefectを達成した。当時の業界平均は10〜50だった。このprocessは文書化され、複数のプロジェクトと言語を横断してreplicateされ、独立して検証された。そして消えた。…
本当に1万行を零欠陥で検証した人がいるのか？IBMはやったし、その方法論は結果より奇妙だ。
Cleanroom software engineeringは、デバッグではなくmathematical verificationによって零欠陥のインクリメントを約束した。我々はIBMの実プロジェクトデータを見て、その主張が成り立ったかを確認する。
1980年代のソフトウェア業界平均は、1000行あたり30〜60の欠陥だった。IBMのCleanroomチームは、2万行のコンパイラインクリメントをテストで53の欠陥を発見した状態で出荷した。これはKLOCあたり2.6である。1万行の個別インクリメントの中には、システムテストで欠陥が全く見つからなかったものもあった。…
あなたのモジュールには3層ある。書いたのは1層だけだろう。
Box Structureは、モジュールが何をするか、何を記憶するか、どう動作するかを、3つの独立した検証可能な層として定義することを強制する。Cleanroomがどうやってデバッグを排除するか、ここで解説する。
まずコードを書き、次にテストを書き、そしてコードが間違っていたことに気づく。これが標準的なループだ。だからデバッグは、ほとんどのプロジェクトのタイムラインの半分を消費する。 Box…
IBM は開発者に自身のコード実行を禁止し、0.1 defects/KLOC のソフトウェアを出荷した
IBM の Cleanroom エンジニアリング・プロセスは、バグを発見するのではなく未然に防ぐことで、業界平均より 100 倍優れた defect 率を達成した。それがどう機能したか、なぜほとんど誰も使わないのか、そして今日あなたが取り入れられるものとは。
IBM は NASA の衛星制御システムを KLOC あたり 0.1 欠陥という水準で出荷した。当時の業界平均は 10 から 50 の間だった。彼らがこれを達成したのは、より優秀な技術者を採用したり、より長時間働いたりしたからではない。開発者に自身のコードを実行することを禁じたからだ。 これが Cleanroom…