Registration info |
一般 ¥1000 (Pre-pay)
FCFS
|
---|---|
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つのバリエーションが考えられます.
- count_pos で仕様を表す.インデックスの昇順に調べる.
- count_pos で仕様を表す.インデックスの降順に調べる.
- card で仕様を表す.インデックスの昇順に調べる.
- card で仕様を表す.インデックスの降順に調べる.
前提知識
- Isabelle Hoare 論理ライブラリ
Media View all Media
If you add event media, up to 3 items will be shown here.