理論計算機科学 において、アルゴリズムが仕様に従って動作する場合、それは仕様に関して正しいとされます。最もよく研究されているのは機能的正しさであり、これはアルゴリズムの入出力動作、すなわち各入力に対して仕様を満たす出力を生成することを指します。[ 1 ]
後者の概念において、返される答えが正しいことを要求する部分的正しさは、最終的に答えが返されること、すなわちアルゴリズムが終了していることをさらに要求する完全正しさとは区別されます。同様に、プログラムの完全正しさを証明するには、部分的正しさと停止性を証明すれば十分です。[ 2 ] 後者の種類の証明（停止性証明）は、停止問題が決定不可能であるため、完全に自動化することはできません。
| 最小の奇数完全数を見つけるための部分的に正しいCプログラム。 2023年時点で完全な正しさは不明。 |
// n の真約数の合計を返します。static int divisorSum ( int n ) { int i , sum = 0 ; for ( i = 1 ; i < n ; ++ i ) if ( n % i == 0 ) sum + = i ; return sum ; } // 最小の奇数完全数を返します。int leastPerfectNumber ( void ) { int n ; for ( n = 1 ; ; n += 2 ) if ( n == divisorSum ( n )) return n ; } |
例えば、1、2、3、…という整数を順に探索し、ある現象（例えば奇数の完全数）の例を見つけることができるかどうかを調べる場合、部分的に正しいプログラムを書くのは比較的簡単です（囲み記事参照）。しかし、このプログラムが完全に正しいと主張することは、数論において現在知られていない何かを主張することになります。
アルゴリズムと仕様の両方が形式的に与えられていると仮定すると、証明は数学的な証明でなければなりません。特に、特定のマシン上でアルゴリズムを実装した特定のプログラムが正しいという主張は想定されていません。その主張には、コンピュータのメモリ制限などの考慮が必要になります。
証明論における深い結果であるカリー・ハワード対応は、構成論理における関数的正しさの証明がラムダ計算における特定のプログラムに対応することを述べています。このように証明を変換することをプログラム抽出と呼びます。
ホーア論理は、コンピュータプログラムの正しさについて厳密に推論するための特定の形式体系です。 [ 3 ]ホーア論理は、プログラミング言語の意味を定義し、ホーアトリプルと呼ばれる主張を通じてプログラムの正しさについて議論するために公理的な手法を使用します。
ソフトウェアテストとは、プログラムやシステムの属性や機能を評価し、それが要求された結果を満たしているかどうかを判断することを目的とした活動です。ソフトウェアの品質にとって非常に重要であり、プログラマやテスターによって広く活用されていますが、ソフトウェアの原理に対する理解が限られているため、ソフトウェアテストは依然として技術の域を出ません。ソフトウェアテストの難しさは、ソフトウェアの複雑さに起因します。中程度の複雑さのプログラムを完全にテストすることはできません。テストは単なるデバッグではありません。テストの目的は、品質保証、検証、妥当性確認、信頼性の推定などです。テストは汎用的な指標としても使用できます。正確性テストと信頼性テストは、テストの2つの主要な領域です。ソフトウェアテストは、予算、時間、品質の間でトレードオフの関係にあります。[ 4 ]
参照
注記
- ^ Dunlop, Douglas D.; Basili, Victor R. (1982年6月). 「機能的正しさの比較分析」 Communications of the ACM . 14 (2): 229– 244. doi : 10.1145/356876.356881 . S2CID 18627112 .
- ^ Manna, Zohar; Pnueli, Amir (1974年9月). 「プログラムの完全な正しさへの公理的アプローチ」. Acta Informatica . 3 (3): 243– 263. doi : 10.1007/BF00288637 . S2CID 2988073 .
- ^ Hoare, CAR (1969年10月). 「コンピュータプログラミングの公理的基礎」(PDF) . Communications of the ACM . 12 (10): 576– 580. CiteSeerX 10.1.1.116.2392 . doi : 10.1145/363235.363259 . S2CID 207726175. 2016年3月4日時点のオリジナル(PDF)からのアーカイブ。
- ^ Pan, Jiantao (1999年春). 「ソフトウェアテスト」（コースワーク）. カーネギーメロン大学. 2017年11月21日閲覧。
参考文献
- 「人間言語技術。コンピュータサイエンスと言語学の課題。」Googleブックス。Np、nd Web。2017年4月10日。
- 「コンピューティングと通信におけるセキュリティ」Googleブックス。Np、nd Web。2017年4月10日。
- 「アラン・チューリングの停止性問題 ― 楽しくてわかりやすい図解」『アラン・チューリングの停止性問題 ― 楽しくてわかりやすい図解』。Np、nd Web。2017年4月10日。
- ターナー、レイモンド、ニコラ・アンギウス。「コンピュータサイエンスの哲学」スタンフォード哲学百科事典。スタンフォード大学、2013年8月20日。ウェブ。2017年4月10日。
- Dijkstra, EW「プログラムの正しさ」テキサス大学オースティン校、数学・コンピュータ科学科、自動定理証明プロジェクト、1970年。Web。
