正確性 (計算機科學)

在理論計算機科學中，算法的正確性（英語：correctness）是指一個算法在程序規範下被認定為正確的判定。其中，功能正確（英語：functional correctness）針對輸入輸出的行為（例如：對每一個輸入，算法都能給出預期的輸出）。^[1]

人們將正確性分為兩類。一類被稱為部分正確性（英語：partial correctness），它要求在算法返回結果時這一結果是正確的；另一類被稱為完全正確性（英語：total correctness），它在部分正確性的基礎之上還要求算法必須能夠結束。由於對於停機問題沒有通用的解決方案，因此判定完全正確性的斷言有著更多需要深層次研究的地方。終止的證明是指一類數學證明，因為完全正確性需要證明一個算法會終止，所以它在程序的形式驗證中起著至關重要的作用。^[2]

例如考慮這樣一個問題：依次搜索整數列1, 2, 3, …來看是否存在某個特定現象——比如說存在一個奇數為完全數。對於這個問題而言，我們很容易寫出一個部分正確的程序（直接對於每個數字做長除法判定其是否完全）。然而如果我們想證明這個程序是完全正確的，那就相當於我們在斷言一個在數論里目前還未知的結論。

在算法和程序規範都是基於形式化來給出時，對正確性的證明應當為一個數學證明。然而我們並不期待能夠給出特定機器上實現的特定程序的正確性斷言，因為那樣將需要考慮諸如內存限制在內的更多問題。

證明論中有一個結論柯里-霍華德同構。這一結論認為：任意一個在構造性邏輯下的功能正確性的證明都對應了一個λ演算程序。這種轉換證明的方式被稱為程序抽出（英文：program extraction）。

霍爾邏輯是一個具體的能夠嚴密驗證程序正確性的形式系統。^[3]它用一系列的公理來定義程序語言的語義，從而通過稱之為霍爾三元組的斷言來驗證程序的正確性。

軟體測試是指驗證一個程序或系統的某些屬性或能力來判斷它是否達到預期目的的行為。儘管軟體測試在軟體質量方面起著至關重要的作用，並且被程式設計師和測試員們廣泛採用，但由於人們對軟體的認識十分有限，它仍舊是一個艱深的領域。軟體測試的最大難點在於如何控制其複雜性：我們沒有辦法在一個合理的複雜度內完整地測試一個程序。測試不只是調試。測試的目的包括但不限於確保軟體質量、驗證其正確性和估算其穩定性。我們對測試的定義也可以更加一般化，其中正確性測試和穩定性測試是兩個最大的研究領域。軟體測試是預算、時間和軟體質量的一個平衡。^[4]

參見

• 形式驗證
• 契約式設計
• 程序分析
• 模型驗證
• 編譯器正確性
• 程序派生