问题描述
我不明白为什么我们使用==>而不是一直使用&&进行隐含。 以我在网上找到的这段代码为例：
var a: array <int> := new int[3];
a[0],a[1],a[2] := 1,1,1;
assert forall j:: 0 <= j < a.length ==> a[j] == 1;
assert exists j:: 0 <= j < a.length && a[j] == 1;
为什么不仅仅使用&&代替含义。因为我们使用的是隐含，所以左侧可以为false，右侧仍然为true。也就是说，数组索引可能超出范围，并且在该索引处，例如a [-10]，元素将为1。a [-10] == 1
解决方法
让我们考虑一下公式
assert forall j:: 0 <= j < a.length && a[j] == 1;
根据您的建议，它使用&&而不是==>。
如果我们用通俗易懂的语言阅读此公式，则它表示“每个整数j都在0到a.length之间，还有a[j] == 1之间”。但这显然是错误的，因为并非每个整数都在0到a.length之间（例如，a.length + 1是不在此范围内的整数）。
因此，在&&下使用forall并没有任何意义。