fixedpoint.jp - Timsort 実装のバグが形式的手法で見つかったけれど... (2015-02-26)

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 プロジェクトに詳細と修正案を報告した