你如何證明一個功能的作品？

Question

我最近得到了測試宗教，並開始主要與單元測試。我編寫的單元測試說明某個功能在某些情況下可以工作，特別是使用我正在使用的確切輸入。我可以做一些單元測試來實現這個功能。儘管如此，我還沒有證明除了函數之外的任何東西，我都希望它在我測試的場景下做。可能還有其他投入和情景我沒有想到，並且邊緣案例的思考代價昂貴，特別是在邊緣。

這對我來說並不是很令人滿意。當我開始考慮不得不提出測試以滿足分支和路徑覆蓋以及集成測試時，未來的排列可能會變得有點瘋狂。因此，我的問題是，怎樣才能證明（在證明數學定理的同一脈絡中）函數是有效的（並且在完美的世界中，將這些「證明」組合成一個證明系統起作用的證據）？

是否有某個測試領域涵蓋了您試圖通過證明其所有功能都能正常工作來驗證系統的方法？學術界以外的任何人都會用這種方法來打擾嗎？有工具和技術可以幫助嗎？

我意識到我對「工作」這個詞的使用並不準確。我想我的意思是說，一個函數在符合某些規範（書面或暗示）聲明它應該做的事情時起作用，除此之外別無其他。

請注意，我不是數學家，只是程序員。

Answer 1

在學術界，有一個類似於數學歸納的概念，它被稱爲結構歸納。但是，它僅適用於函數式編程語言和完全沒有副作用的方法。在另一些情況下，即使不是不可能，也很難證明某種方法是由於副作用而起作用的。

在TDD中，您嘗試制定方法必須滿足的邊緣情況，但是，可能會錯過這種情況。即使一個（非平凡的）方法滿足你所有的測試，也可能有一些參數或一系列事件的組合，你根本沒有想到這會破壞你的代碼。簡單地說：就是生活。你可以在一個非平凡的實現中預測所有結果，但是你可以確保該方法適用於特定的邊緣情況，期望某些情況如此尖銳，你會在觸摸它們時削減自己。 （zing，壞雙關）。

Answer 2

聽起來好像你正在將工作定義爲做你想做的事情。換句話說，你想證明你正確地輸入了邏輯。

那麼，在這種情況下，至少假設一個函數接近無限量的有效輸入，你不能真正證明某件事是正確的，你只能反駁它。所以這個想法是創建跨功能的各種輸出的良好單元測試。它沒有證明是正確的，但可以用來證明某件事是正確的。

Answer 3

通過正式證明可以做到證明某件事情有效的方法。至少在學術界，一些技術是衆所周知的。想到的是"Proof by induction"。但是，這種方法是相當手動的，而且對於凡人來說也相當容易出錯，如果不是簡單的話太複雜。

形式驗證的另一種更易於管理的方法被稱爲「模型檢查」。通過這種方法，您可以以適當的方式表達您的軟件，從而使您可以對其執行某些檢查（使用工具）。一個這樣的檢查可能是檢查多線程應用程序中的死鎖/活鎖。 您可以執行的其他類型的檢查是確保您的應用程序始終允許與同一應用程序的更簡單模型進行相同類型的交互，從而降低在模型中犯同樣錯誤的機會和真正的應用程序。模型檢查工具可能是Spin，但有很多。

看來，維基百科對這個題目太大了一篇文章：Formal Verification

Answer 4

「這聽起來像你規定了工作的功能做你想讓它做什麼」 通常你還需要驗證函數不會做你不想做的事情，這些定義是接近但不相同的，例如一個ADD（）函數可以返回正確的答案，但也會打印出一些額外的調試垃圾。