プログラム正当性検証のための構造化（1967年のノート）
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/04/25 06:17 UTC 版)
「構造化プログラミング」の記事における「プログラム正当性検証のための構造化（1967年のノート）」の解説
ダイクストラは、プログラマは正しいプログラムを作り出すばかりでなく納得のいくやり方で正しさを証明（検証）することも仕事の一つであるという立場を取っていた。プログラムがどんなに巨大化しても良く構造化（well-structured）されていれば、サイズに関係なくその正当性を検証できるというのが彼の信念であった。well-formed formula（論理式）に因んでいるwell-structuredには、数理論理学の証明論をソースコードにも導入する意図が込められていた。1967年のノート「Towards Correct Programs」でダイクストラは、良く構造化するための三つのメンタルツール（mental tool）をこのように示している。 列挙（enumeration）： 一人の人間の能力でできる範囲でプログラムの命令の妥当性を一つ一つ確認していく作業 数学的帰納（mathematical induction）： while文など計算機特有の多数の繰り返し文についてのみ数学的帰納法を用いて確認する作業 抽象（abstraction）： プログラムのブロックなどに名前をつけ、さらに中身を見ないで正しいと仮定することで検証作業を後回しにする操作 プログラムが正しいことを確認するには、それを証明しなければならない。テストはプログラムに対する疑いを全て取り除くには不十分であるという意見が上がった。これについてダイクストラは「テストはバグの存在を示すには有効だが、バグが存在しないことは証明できない」という表現を好んで用いた。構造化プログラミングの支持者らは、プログラムの正しさの重要性と証明の方法や表明(assertion)の使い方について熱心に説いた。理想的にはテストだけに依存せず、プログラムの正しさの証明も与えるべきだと言われている。所与のプログラムの正しさを後付けで証明することは、はじめから証明を意識して作られたプログラムの場合より難しいことが経験的に知られている。ダイクストラは、プログラミングと同時にプログラムの証明を（わずかに証明を先行して）進めることを推奨している。そのようなアプローチでプログラムの正当性の問題にあたれば、複雑な問題であっても知的管理が可能であると述べた。しかし形式的な証明は、時として非人間的な長さの記述になることもダイクストラは認めている。同氏は、プログラムの証明が形式的であることにはこだわらないという意見を明らかにした。
※この「プログラム正当性検証のための構造化（1967年のノート）」の解説は、「構造化プログラミング」の解説の一部です。
「プログラム正当性検証のための構造化（1967年のノート）」を含む「構造化プログラミング」の記事については、「構造化プログラミング」の概要を参照ください。
- プログラム正当性検証のための構造化のページへのリンク
