フォーマル検証

ウィキペディア小見出し辞書

フォーマル検証

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/08/18 08:12 UTC 版)

「ティムソート」の記事における「フォーマル検証」の解説

2015年、EU FP7 ENVISAGEプロジェクトのオランダとドイツの研究者は、ティムソートの標準実装にバグを発見しました。 具体的には、スタックされた配列サイズの不変量により、必要なスタックの最大サイズの上限が厳しくなります。実装は、2 64バイトの入力をソートするのに十分なスタックを事前に割り当て、それ以上のオーバーフローチェックを回避しました。 ただし、保証では、不変条件を3回の連続配列のすべてのグループに適用する必要がありますが、実装では上位3つのみをチェックしました。 研究者は、Javaソフトウェアのフォーマル検証にKeYツールを使用して、このチェックでは不十分であり、スタックのより深いところで不変条件に違反する結果となるランレングス（およびそれらのランレングスを生成した入力）を見つけることができました。スタックの最上位がマージされた後。 結果として、特定の入力では、割り当てられたサイズは、マージされていないすべての配列を保持するのに十分ではありません。 Javaでは、これにより、これらの入力に対して配列外の例外が生成されます。 JavaおよびAndroidv7でこの例外をトリガーする最小の入力は、サイズ67108864 （2 26 ）です。 65536 （2 16 ）の特定の入力に対してこの例外が既にトリガーされています） Javaの実装は、更新された最悪の場合の分析に基づいて、事前に割り当てられたスタックのサイズを増やすことによって修正されました。この記事では、スタック内の最上位の4つの配列が上記の2つのルールを満たしていることを確認することにより、目的の不変条件を確立する方法も形式手法で示しました。このアプローチは、Python とAndroidで採用されました。