2016-05-01から1日間の記事一覧

二分探索に証明を付ける

Coq OCaml

二分探索は言わずと知れた探索アルゴリズムですが、実際に実装しようとすると無限ループしたり正しい答えが得られなかったりする事も多いのではないでしょうか。そこで、ここではCoqで二分探索を実装し、正当性の証明を行いました。