証明ドリル (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 論理ライブラリ