お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
2024年5月23日(木)以降より開始予定の「connpass 有料API」の料金プランにつきましてはこちらをご覧ください。
なお有料の対象となるのはAPIのみであり、connpassのサービスにつきましては今後も無料でご利用いただけます。

6月

15
ヒープソート siftup の正当性証明

ハッシュタグ：#形式手法

募集内容	一般無料先着順 6/10人
申込者	申込者一覧を見る
開催日時	2021/06/15(火) 20:30 ～ 22:00 Googleカレンダー icsファイル
募集期間	2021/06/15(火) 00:00 〜 20:00まで
会場	Zoom オンライン

イベントの説明

イベントの内容

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

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

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

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

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

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