プログラム検証の視点

プログラム検証に対する1人の視点と、それが信頼性のあるソフトウェアのいくつかの側面との関係が示されている。主な検証法である帰納的主張は、1つの詳細な例のいくつかのバリエーションを用いて説明される。2つ目の例では、反復的な木のトラバーサルの例に対する驚くほど簡単な帰納的主張の証明が示される。また、ほとんどの検証に対する暗黙の前提、終了の証明、主張の作成、および主張を書くための言語についても簡単に議論されている。既存のプログラム検証システムの概要と、検証されたプログラムのサンプルリストが提供される。短い参考文献も含まれている。