『定理証明手習い』

プログラムの正しさは証明できる。定理証明へ踏み出すための最高のガイドブック

• Daniel P. Friedman, Carl Eastlund 著、中野圭介 監訳
• 240ページ
• A5判
• ISBN：978-4-908686-02-3
• 2017年10月23日 第1版第1刷 発売

あるプログラムが、考えられるあらゆる入力に対して誤った動作を引き起さないことは、テストを書いても確かめられません。それを確かめるには、公理と式の等価な書き換えだけで恒真を導いたり、再帰的なプログラムの構造に照した帰納法による証明が必要です。

なんだか難しそうに聞こえるかもしれませんが、その世界観を丁寧にときほぐして解説したのが、本書の原書にあたる "The Little Prover" です。