Java や Python で広く利用されている Timsort というソートアルゴリズムの実装のバグを形式的手法で見つけたというニュースがありました: http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
Design by Contract の考え方に基づいた KeY というツールで正しさを検証しようとしたところ、証明できなかったのでよく調べてみたらバグがあったということです。KeY では関数が評価される際の事前条件と事後条件、および不変条件を表現でき、関数内の全てのパスでこれらの条件が成り立っているかどうかを静的に証明できるそうです。
冒頭の記事に書かれているように、発見者は OpenJDK プロジェクトに詳細と修正案を報告したのですが、その反応は期待通りではなかったようです:
The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space. Given the astronomical number of program runs that such a central routine is used in, this leads to a considerable waste of energy. As to the reasons, why our solution has not been adopted, we can only speculate: perhaps the JDK maintainers did not bother to read our report in detail, and therefore don’t trust and understand our fix. After all, Open Java is a community effort, largely driven by volunteers with limited time.
実際のバグ報告を見てみると、実は発見者自身が2つの修正案を示しており、コミットされた修正はその1つ(現実的なケースにおいて十分なメモリを確保するように変更)を採用しています。そのため、発見者が採用して欲しかったもう1つの案が無視された形になったということです。
しかし、これはバグ報告のためのコミュニケーションに改善の余地があったと言えそうです。おそらく報告の中で単独の修正案を示していたら、それが採用された可能性が高かったはずです。(さらにパッチとして提供されていたらさらに望ましかったはずです。というのも、その変更による影響範囲がどれくらいかを確認するのに差分の形が便利だからです。)また、発見者が想像から言及している "volunteers with limited time" というのもやや乱暴です。なぜなら、今回修正を担当した開発者も(メールアドレスから判断すると)Oracle に所属しており、職務の一環として活動していると考えられるためです。
今回の教訓としては、たとえ形式的手法で不具合を発見し証明できても、望ましい修正を提案する過程が重要であることは変わらない、ということになります。