# 大夫。没有发现触发的条件是什么意思？[英] Dafny: What does no terms found to trigger on mean?

### 问题描述

No terms found to trigger on.

```method sqrt(n : nat) returns (r: int)
// square less than or equal to n
ensures (r * r) <= n
// largest number
ensures forall i :: 0 <= i < r ==> (i * i) < (r * r)
{
var i := 0; // increasing number
r := 0;
while ((i*i) <= n)
invariant (r*r) <= n
invariant forall k :: 0 <= k < r ==> (k*k) < (r*r)
decreases n - i
{
r := i;
i := i + 1;
}

return r;
}
```

Dafny 告诉我这是一个警告.这是否意味着我的量词是错误的?或者这是否意味着 Dafny 根本无法验证它但它是正确的?

## 推荐答案

```function square(n: int): int
{
n * n
}

method sqrt(n : nat) returns (r: int)
// square less than or equal to n
ensures r * r <= n
// largest number
ensures forall i :: 0 <= i < r ==> square(i) < r * r
{
var i := 0; // increasing number
r := 0;
while i * i <= n
invariant r * r <= n
invariant forall k :: 0 <= k < r ==> square(k) < r * r
decreases n - i
{
r := i;
i := i + 1;
}

return r;
}
```

<小时>

## 什么是触发器?

```forall x {:trigger P(x)} :: P(x) && Q(x)
```

```method test()
requires forall x {:trigger P(x)} :: P(x) && Q(x)
ensures Q(0)
{
}
```

Dafny 抱怨它无法验证后置条件.但这在逻辑上是显而易见的！只需在前置条件中为 x 插入 0 即可得到 P(0) && Q(0)，这意味着后置条件 Q(0).

```assert P(0);
```

(顺便说一句，请注意，如果我们让 Dafny 推断触发器而不是手动阻止它，则此示例在没有不相关的断言的情况下通过.)