Oz - プログラミング概念入門(プログラムの正しさ, 数学的帰納法)

コンピュータプログラミングの概念・技法・モデル
(IT Architect' Archive
クラシックモダン・コンピューティング6)
(IT Architects’Archive CLASSIC MODER)
(翔泳社)
セイフ・ハリディ (著), ピーター・ヴァン・ロイ (著)
Peter Van-Roy (著), Seif Haridi (著), 羽永 洋 (翻訳)
原書: Concepts, Techniques,
and Models of Computer Programming

開発環境

• OS X Yosemite - Apple (OS)
• Emacs (Text Editor)
• Oz (プログラミング言語)
• Mozartプログラミングシステム(Mozart 2) (実装)

コンピュータプログラミングの概念・技法・モデル(IT Architect' Archiveクラシックモダン・コンピューティング6) (IT Architects’Archive CLASSIC MODER)(セイフ・ハリディ (著)、ピーター・ヴァン・ロイ (著)、Peter Van-Roy (著)、 Seif Haridi (著)、羽永 洋　(翻訳) 、翔泳社、原書: Concepts, Techniques, and Models of Computer Programming(CTM))の第1章(プログラミング概念入門)、1.18(練習問題)、3.(プログラムの正しさ)を解いてみる。

3.(プログラムの正しさ)

1. {Pascal 1}は、正しい答、[1]を返す。
2. {Fact N-1}が正しいと仮定する。(N > 2)
   1. if文のelse部分が実行される。
   2. {AddList {ShiftLeft {Pascal N-1}} {ShiftRight {Pascal N-1}|}}が呼ばれる。
   3. {ShiftLeft {Pascal N-1}}、{ShiftRight {Pascal N-1}}が呼ばれる。
   4. 仮定により、{Pascal N-1}は正しい答を返す。
   5. よって、ShiftLeft、ShiftRight、AddListが正しいとすれば、{Pascal N}も正しい答を返す。

ShiftLeft関数について。

1. {ShiftLeft nil}は正しい答、すなわち[0]を返す。
2. Lを要素の個数が1以上で、頭部がH、尾部がTのリストとし、{ShiftLeft T}が正しいと仮定する。
   1. {ShiftLeft L}の呼び出しをみる。
   2. H|{ShiftLeft T}が計算される。
   3. 仮定より{ShiftLeft T}は正しい答を返す。
   4. よって、|(リンク、cons)が正しいとすれば、{ShiftLeft L}も正しい答を返す。

ShiftRight関数は正しい答を返す。

AddList関数について。

1. {AddList nil nil}は正しい答、すなわちnilを返す。
2. 任意のリストLに対し、{AddList nil L}は正しい答、すなわちnilを返す。
3. L1を要素の個数が1個以上のリストとし、その頭部をH1、尾部をT1とする。
   1. {AddList L1 nil}は正しい答、すなわちnilを返す。
   2. L2を要素の個数が1個以上のリスト、H1をL2の頭部、T2をL2の尾部とし、{AddList T1 T2}が正しいと仮定する。
      1. {AddList L1 L2}の呼び出しを見る。
      2. H1+H2|{AddList T1 T2}が計算される。
      3. 仮定より、{AddList T1 T2}は正しい答を返す。
      4. よって、|(リンク、cons)が正しいとすれば、{AddList L1 L2}も正しい答を返す。