この記事での学習内容 応用情報

プログラムの正当性理論とは何か、部分正当性、全正当性の基本的な考え方、仕組みを理解する。

用語例： 停止問題

 

プログラムの正当性

プログラム開発においては、不具合（＝バグ）の発生はなかなか避けられないものです。このバグの除去のために作成するプログラムに対して、テストや検証を行いますが、「検証」を行うことで、プログラムの正当性を証明することができます。

ここでいう「プログラムの正当性」とは、「入力条件を満たしたプログラムを実行すると、そのプログラムは確実に停止するとともに出力条件を満たした結果が得られる」ということを指します。完全正当性とも言います。

部分正当性

正当性のうち、「入力条件を満たしたプログラムを実行すると、そのプログラムは出力条件を満たした結果が得られる」ことを部分正当性といいます。

停止性

正当性のうち、「そのプログラムは確実に停止する」ことを停止性といいます。

プログラムの検証において、停止性を証明するためには、特にプログラム内の繰り返し（ループ）部分に着目します。繰り返しの条件が不適切な場合、プログラムが永久に終了しない（＝無限ループ）状態となってしまい、停止性を満たすことができません。

停止性問題

計算可能性理論において停止(性)問題（ていしせいもんだい・ていしもんだい、halting problem）は、あるチューリング機械（≒コンピュータプログラム・アルゴリズム）が、そのテープのある初期状態（≒入力）に対し、有限時間で停止するか、という問題。アラン・チューリングが1936年、停止性問題を解くチューリング機械が存在しない事をある種の対角線論法のようにして証明した。すなわち、そのようなチューリング機械の存在を仮定すると「自身が停止すると判定したならば無限ループを行い、停止しないと判定したならば停止する」ような別のチューリング機械が構成でき、矛盾となる。

Wikipediaから引用