什么是谓词检查？

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是 后置条件谓词。