静的解析は飛行機が墜落しないことを証明できない。だが、もっと有益なことは証明できる。
抽象解釈はあらゆる可能なプログラム状態を過大近似する。抽象化の中でゼロ除算が到達不可能なら、実際のコードでも到達不可能である。以下に、その仕組みと限界を解説する。
静的解析は、飛行機が墜落しないことを証明することはできない。しかし、高度計の制御ループが決してゼロ除算を起こさないこと、配列の範囲外を決して参照しないこと、固定小数点アキュムレータが決してオーバーフローしないことは証明できる。この区別が重要なのは、一方は物理、空気力学、そして応力下のアルミニウムに関する主張であり、他方…