text: 在理論計算機科學中，演算法的正確性。人們將正確性分為兩類。一類被稱為部分正確性，它在部分正確性的基礎之上還要求演算法必須能夠結束。由於對於停機問題沒有通用的解決方案，因此判定完全正確性的斷言有著更多需要深層次研究的地方。終止的證明是指一類數學證明，因為完全正確性需要證明一個演算法會終止，所以它在程式的形式驗證中起著至關重要的作用。例如考慮這樣一個問題：依次搜尋整數列1, 2, 3, …來看是否存在某個特定現象——比如說存在一個奇數為完全數。對於這個問題而言，我們很容易寫出一個部分正確的程式。然而如果我們想證明這個程式是完全正確的，那就相當於我們在斷言一個在數論裡目前還未知的結論。在演算法和程式規範都是基於形式化來給出時，對正確性的證明應當為一個數學證明。然而我們並不期待能夠給出特定機器上實現的特定程式的正確性斷言，因為那樣將需要考慮諸如記憶體限制在內的更多問題。證明論中有一個結論柯里-霍華德同構。這一結論認為：任意一個在構造性邏輯下的功能正確性的證明都對應了一個λ演算程式。這種轉換證明的方式被稱為"程式抽出"。霍爾邏輯是一個具體的能夠嚴密驗證程式正確性的形式系統。它用一系列的公理來定義程式語言的語義，從而透過稱之為霍爾三元組的斷言來驗證程式的正確性。軟體測試是指驗證一個程式或系統的某些屬性或能力來判斷它是否達到預期目的的行為。儘管軟體測試在軟體質量方面起著至關重要的作用，並且被程式設計師和測試員們廣泛採用，但由於人們對軟體的認識十分有限，它仍舊是一個艱深的領域。軟體測試的最大難點在於如何控制其複雜性：我們沒有辦法在一個合理的複雜度內完整地測試一個程式。測試不只是除錯。測試的目的包括但不限於確保軟體質量、驗證其正確性和估算其穩定性。我們對測試的定義也可以更加一般化，其中正確性測試和穩定性測試是兩個最大的研究領域。軟體測試是預算、時間和軟體質量的一個平衡。
metadata: erhwenkuo/wikipedia-zhtw
metadata: 正確性 (計算機科學)
metadata: https://zh.wikipedia.org/wiki?curid=6425860