-
紙書籍をお届けします（PDFがついてきます）
- PDFは購入後すぐにダウンロード可能です
- 紙書籍は通常、ご注文から2～3営業日で発送します
- 年末年始や大型連休など、1週間から10日程度、配送のお休みをいただく場合があります。詳しくはお知らせをご覧ください
プログラムの正しさは証明できる。定理証明へ踏み出すための最高のガイドブック
- Daniel P. Friedman, Carl Eastlund 著、中野圭介 監訳
- 240ページ
- A5判
- ISBN：978-4-908686-02-3
- 2017年10月23日 第1版第1刷 発行
- 正誤情報
あるプログラムが、考えられるあらゆる入力に対して誤った動作を引き起さないことは、テストを書いても確かめられません。それを確かめるには、公理と式の等価な書き換えだけで恒真を導いたり、再帰的なプログラムの構造に照した帰納法による証明が必要です。
なんだか難しそうに聞こえるかもしれませんが、その世界観を丁寧にときほぐして解説したのが、本書の原書にあたる "The Little Prover" です。
執筆者紹介
Daniel P.Friedman（原著者）
インディアナ大学計算機科学科教授。著書に“The Little Schemer (fourth edition)”（ 邦題『Scheme手習い』）、“The Reasoned Schemer”、“The Seasoned Schemer” （邦題『Scheme 修行』）、“Essentials of Programming Languages (third edition)” （以上、The MIT Press）。
Carl Eastlund（原著者）
ソフトウェアエンジニア。Jane Street Capital（ニューヨーク）勤務。
中野圭介（監訳者）
東京大学理学部数学科中退。京都大学大学院理学研究科数学・数理解析専攻数理解析系博士後期課程単位取得退学。東京大学大学院情報理工学系研究科産学官連携研究員などを勤め、現在、電気通信大学大学院情報理工学研究科准教授。
証明支援系、関数型プログラミング、形式言語理論、双方向変換に関する研究に従事しつつ「ジグソーパズルによる関数型プログラミング」や「余帰納的にジャグリングをしよう（訳題）」など風変わりな論文も執筆。博士（理学）。
目次
((目次)
(監訳者序文)
(序文)
(はじめに)
(((1.いつものゲームに新しいルールを)) (例))
(((2.もう少し、いつものゲームを)) (例))
(((3.名前に何が？)) (証明))
(((4.これが完全なる朝食)) (証明))
(((5.何回も何回も何回も考えよう)) (証明))
(((6.最後まで考え抜くのです)) (証明))
(((7.びっくりスター！)) (証明))
(((8.これがルールです)) (証明))
(((9.ルールを変えるには)) (証明))
(((10.いつかはスターで一直線)) (証明))
((A.放課後))
((B.デザートには証明を))
((C.小さなお手伝い))
((D.休んでなんていられない？))
(あとがき)
(索引))
