什麼是謂詞檢查？

Question

我已經搜索了一段時間，但無法找到關於「謂詞檢查」的簡明定義。我們什麼時候可以應用謂詞檢查？它與Hoare的三倍相比如何？我認爲如果我們將Hoare的三元組正確應用於每行代碼，我們可以保證軟件的正確性。 （如果我錯了，請糾正我。）謂詞檢查是否可以提供相同的屬性？如果問題本身不正確，我很抱歉。我真的不知道謂詞檢查做了什麼。

Answer 1

A 謂詞是一個邏輯語句或函數，它等同於真或假的結果。

程序語言和聲明語言中謂詞的最簡單的例子是guard子句和斷言例如

> if (x != null) then ... 
> assert x != null 

霍爾的先決條件和後置條件是謂詞的例子。我不認爲Hoare中有關封裝語句的粒度的任何明確信息，前提是它具有單個退出路徑進入後置條件。它可以是單個陳述，功能或整個過程。

不變量是謂詞的特例，其中後置條件=前置條件。

也許這個最純粹的例子是Prolog，其中每個陳述是一個謂詞。另一個例子是Eiffel中使用的按合同設計，而LISP中的空白列表也是謂詞。

我不願意同意「保證軟件的正確性」，沒有正確性符合謂詞的限定。

更新

• 的Assume in JUnit和BDD給定的前提條件 謂詞。
• Assert in JUnit and Then BDD是 後置條件謂詞。