0

我正在与 Boogie 合作，我遇到了一些我不理解的行为。

我一直在用assert(false)它来检查前面的assume陈述是否荒谬。

例如在以下情况下，程序被验证没有错误......

type T;
const t1, t2: T;
procedure test()
{
  assume (t1 == t2);
  assume (t1 != t2);
  assert(false);
}

......这t1 == t2 && t1 != t2是一个荒谬的说法。

另一方面，如果我有类似的东西

type T;
var map: [T]bool;
const t1, t2: T;

procedure test()
{
  assume(forall a1: T, a2: T :: !map[a1] && map[a2]);
  //assert(!map[t1]);
  assert(false);
}

唯一在assert(false)注释行未注释时失败。为什么评论断言改变了结果assert(false)？

4

1 回答 1

3

要点：如果您map[...]在程序中未提及 的地面实例，Boogie 底层的 SMT 求解器将不会实例化量词。

原因如下：SMT 求解器（使用电子匹配）通常使用句法启发法来决定何时实例化量词。考虑以下量词：

forall i: Int :: f(i)

这个量词允许无限多的实例化（因为i范围在一个无界域上），因此尝试所有将导致非终止。相反，SMT 求解器期望句法提示指示它i应该为哪个量词实例化。这些提示称为模式或触发器。在 Boogie 中，它们可以这样写：

forall i: Int :: {f(i)} f(i)

此触发器指示 SMT 求解器实例化程序中提到的每个量词i（f(i)或者更确切地说，当前证明搜索）。例如，如果您假设f(5)，那么量词将被实例5化为i。

在您的示例中，您没有明确提供模式，因此 SMT 求解器可能会通过检查量词主体为您选择一个。它很可能会选择{map[a1], map[a2]}（允许多个功能应用程序，模式必须涵盖所有量化变量）。如果取消注释该假设，则基本项map[t1]变为可用，并且 SMT 求解器可以使用a1, a2映射到实例化量词t1, t1。因此，得到了矛盾。

有关模式的更多详细信息，请参阅Z3 指南。有关模式的更多相关文本可以在本文中找到，例如在 本文中、在 本文中或在 本文中。

于 2017-03-24T06:49:25.000 回答