<分区>
我已经搜索了一段时间，但找不到关于“谓词检查”的简明定义。我们什么时候可以应用谓词检查？它与 Hoare 的三重奏相比如何？我认为如果我们正确地将霍尔三元组应用于每一行代码，我们就可以保证软件的正确性。 (如果我错了，请纠正我。)谓词检查可以给出相同的属性吗？如果问题本身格式错误，我深表歉意。我真的不知道谓词检查有什么作用。
<分区>
我已经搜索了一段时间，但找不到关于“谓词检查”的简明定义。我们什么时候可以应用谓词检查？它与 Hoare 的三重奏相比如何？我认为如果我们正确地将霍尔三元组应用于每一行代码，我们就可以保证软件的正确性。 (如果我错了，请纠正我。)谓词检查可以给出相同的属性吗？如果问题本身格式错误，我深表歉意。我真的不知道谓词检查有什么作用。
最佳答案
谓词 是一个逻辑语句或函数，等同于真或假结果。
过程性和声明性语言中谓词的最简单示例是保护子句和断言，例如
> if (x != null) then ...
> assert x != null
Hoare 中的前置条件和后置条件是谓词的示例。我不认为 Hoare 中有任何关于封装语句粒度的明确内容，前提是它有进入后置条件的单一退出路径。它可以是单个语句、函数或整个过程。
不变量是谓词的特例，其中后置条件 = 前置条件。
或许这方面最纯粹的例子是 Prolog，其中每个语句 都是一个谓词。又如Eiffel中的design-by-contract，LISP中的空表也是predicate。
我不愿意同意“保证软件的正确性”，如果没有正确性符合谓词的条件的话。
更新
关于unit-testing - 什么是谓词检查？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/9446461/