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

Jul

20

証明ドリル (1) プログラムの証明練習 in Isabelle

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

一般

1000 (Pre-pay)

FCFS
7/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.CONNPASS上でキャンセルしても,セミナー当日に不参加であったとしても参加費用は返却されません.

Print receipt data:

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

Description

証明ドリル (1) プログラムの証明練習 in Isabelle

プログラムでは数を数えることが頻繁にあります.そこで数を数えるプログラムに関する証明の練習しませんか?

以下に問題を書くので挑戦してみてください.答えの解説を聞きたい人はイベントに申し込んでください.

有限集合の要素の数 card

有限集合 A の要素の数は card A と表すことができます.たとえば整数のリスト(または配列)v の要素のうち,正である要素の数は次のように表すことができます.正である要素のインデックスの数を数えるわけです.

card {i. i < length v & v ! i > 0}

これを求めるプログラムを考えることにします.

尚,card に関する定理は Finite_Set.thy の中にあります.

問題 1

整数のリストに含まれる正の要素の数を求める関数 count_pos を定義してください.

問題 2

次の式を証明してください.

count_pos v = card {i. i < length v & v ! i > 0}

問題 3

整数の配列に含まれる正の要素の数を求める命令型のプログラムを書いて,正当性を証明してください.

4つのバリエーションが考えられます.

  1. count_pos で仕様を表す.インデックスの昇順に調べる.
  2. count_pos で仕様を表す.インデックスの降順に調べる.
  3. card で仕様を表す.インデックスの昇順に調べる.
  4. card で仕様を表す.インデックスの降順に調べる.

前提知識

  • Isabelle Hoare 論理ライブラリ

Media View all Media

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

Group

PRINCIPIA

Number of events 82

Members 226

Ended

2020/07/20(Mon)

20:30
22:00

Registration Period
2020/07/14(Tue) 00:00 〜
2020/07/20(Mon) 20:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(7)

elkel53930

elkel53930

証明ドリル (1) プログラムの証明練習 in Isabelleに参加を申し込みました!

niszet

niszet

証明ドリル (1) プログラムの証明練習 in Isabelle に参加を申し込みました!

shigemi1014

shigemi1014

I joined 証明ドリル (1) プログラムの証明練習 in Isabelle!

Kuniwak

Kuniwak

証明ドリル (1) プログラムの証明練習 in Isabelle に参加を申し込みました!

tukejonny

tukejonny

証明ドリル (1) プログラムの証明練習 in Isabelle に参加を申し込みました!

IKEBE Ryohji

IKEBE Ryohji

証明ドリル (1) プログラムの証明練習 in Isabelle に参加を申し込みました!

TakeshiHori

TakeshiHori

証明ドリル (1) プログラムの証明練習 in Isabelle に参加を申し込みました!

Attendees (7)