新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

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

May

7

tackeさんからの挑戦状

Isabelleによるプログラムの正当性証明事例解説

Organizing : PRINCIPIA Limited

Hashtag :#FormalVerification
Registration info

一般

Free

FCFS
3/10

「証明には甘いお菓子が必要」支援

500 (Pre-pay)

FCFS
3/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

支援ありがとうございます。

Print receipt data:

発行しない (詳しくはこちら)

Description

tacke さんからの挑戦状

初谷@PRINCIPIAです.

セミナーに参加していた tacke さん(仮名)から挑戦状が届きました。

君にこの問題が証明できるかな?

2つの列 xs と ys を考えよう。ys の各要素は xs の要素でもあり、対応する要素の並び順は xs 上でのインデックス順になっているとき、ys は xs のサブシーケンスであるという。サブシーケンスであるかどうかを判定するプログラムを書き、正当性を証明してごらん。

subsequence

挑戦を受けた私は Isabelle で証明を試みました。その過程をそのまま解説したいと思います。整理された証明と違って追うのはたいへんかもしれませんが、試行錯誤の過程も含めてどんなふうに考え、どんなふうに証明しているのか一例を紹介する機会にしたいと考えました。調べるべき可能性はまだありますが、一応プログラムの証明ができたところまでにします。

お菓子と飲み物など用意して気軽に聞いてください.途中参加・途中退出はご自由にどうぞ.

Isabelle の理論ファイルと Zoom の URL は CONNPASS のメッセージでお知らせします.

Media View all Media

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

Feed

hatsugai

hatsugai published tackeさんからの挑戦状.

05/05/2020 00:33

Ended

2020/05/07(Thu)

19:30
21:00

Registration Period
2020/05/05(Tue) 00:00 〜
2020/05/07(Thu) 19:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(6)

asya-kawai

asya-kawai

tackeさんからの挑戦状 に参加を申し込みました!

takumi-kato

takumi-kato

tackeさんからの挑戦状に参加を申し込みました!

Incognito

Incognito

tackeさんからの挑戦状 に参加を申し込みました!

niszet

niszet

tackeさんからの挑戦状 に参加を申し込みました!

tacke_jp

tacke_jp

昨日相談させてもらった内容が早速セミナーに!?笑 ありがとうございます、live proofing楽しみです。

Kuniwak

Kuniwak

tackeさんからの挑戦状に参加を申し込みました!

Attendees (6)

Canceled (1)