このエントリーをはてなブックマークに追加

Jun

15

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

Hashtag :#形式手法
Registration info

一般

Free

FCFS
6/10

Description

イベントの内容

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

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

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

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

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

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

Media View all Media

If you add event media, up to 3 items will be shown here.

Group

PRINCIPIA

Number of events 96

Members 245

Ended

2021/06/15(Tue)

20:30
22:00

Registration Period
2021/06/15(Tue) 00:00 〜
20:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(6)

mrsekut

mrsekut

ヒープソート siftup の正当性証明 に参加を申し込みました!

kamada_tatuya

kamada_tatuya

I joined ヒープソート siftup の正当性証明!

TakeshiHori

TakeshiHori

ヒープソート siftup の正当性証明 に参加を申し込みました!

Yusuke Kataoka

Yusuke Kataoka

ヒープソート siftup の正当性証明に参加を申し込みました!

totomaru

totomaru

ヒープソート siftup の正当性証明 に参加を申し込みました!

sawaragikun

sawaragikun

ヒープソート siftup の正当性証明 に参加を申し込みました!

Attendees (6)