イベントの内容

ヒープソートで使われる siftup という手続きの正当性証明を解説します。

siftup とは1か所だけヒープとしての条件を満たさない配列を条件を満たすように再構築する手続きです。

Programming Pearls （邦訳：珠玉のプログラミング、またはプログラム設計の着想）という本の中にヒープソートについてのコラムがあります。そこで著者の Bentley はあるループ不変条件を設定して証明のスケッチを示しているのですが、条件が弱いと Knuth から指摘された話が脚注があります。このあたりの話をします。

証明は定理証明支援系 Isabelle/HOL を使って行います。

飲み物とお菓子でも用意して気軽に聞いてください。

参加申し込み締め切り後に Zoom meeting の URL を connpass のメッセージでお知らせします。