『定理証明手習い』の読み方（私論） - golden-luckyの日記

本記事は、ラムダノートで発売している『定理証明手習い』を買っていただいた方に「読んで」とお願いするための「私家版、読み方のおすすめ」です。そもそも定理証明とか自分には関係ないしっていう人も多いと思うので、「気になるけど買ってない」という方に興味を持ってもらうことも目的としています。 「ラムダノートの本の読み方（私論）」シリーズはこれで第3回なのですが、前回からは丸1年も空いてしまいました。この間に『実践プロパティベーステスト』を出版し、プログラムの挙動を検証する本について語れることが増えたので、そのあたりの世界観自体から話を始めていきたいと思います。 テストケースを手作りして挙動を確かめる 性質からテストケースを自動生成するプロパティベーステスト プログラムの性質を値によらず「証明」する 証明してみよう 続きは『定理証明手習い』で 現実的な効能？ テストケースを手作りして挙動を確かめる 配

[mumei-0]

“あらゆる値に対して必ず何らかの値を返して停止するという性質（「全域性」とか「停止性」などと呼ばれます）”