达芙妮。无法确定 LHS 的存在......对于序列答案

【问题标题】：Dafny. Cannot establish the existence of LHS ... for sequences达芙妮。无法确定 LHS 的存在......对于序列
【发布时间】：2019-11-01 23:08:57
【问题描述】：

对于以下代码，我得到它无法确定满足这样的谓词的 LHS 值的存在。我怎样才能证明右边成立并且这样的 x 存在？

method Main() {
  var n : int := 10;
  var x : seq<int> :| n == |x| && forall i :: 0 <= i < |x| ==> -1 <= x[i] <= 1; 
}

https://rise4fun.com/Dafny/TiO5

【问题讨论】：

标签： dafny

【解决方案1】：

您需要提供证人。以下断言可以解决问题：

method Main() {
  var n : int := 10;
  assert |[0, 0, 0, 0, 0, 0, 0, 0, 0, 0]| == 10;
  var x : seq<int> :| n == |x| && forall i :: 0 <= i < |x| ==> -1 <= x[i] <= 1; 
}

但是，这会将您带到下一点，那就是

【讨论】：

这不起作用...我得到Error: this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable 'x'
我本来打算在上面评论这个作为“下一点”，但显然我的句子不知何故被切断了。此错误消息表明验证程序现在能够证明 x 的值存在，但编译器仍然无法弄清楚如何为其生成代码。

【解决方案2】：

目前似乎连这样的小事都不支持：

method Main() {
  var n : int := 10;
  var y : seq<int> :|  y  == [3];
  var x : seq<int> :|  x  ==  y;
  var z : seq<int> :| |z| == |y|;
}

Dafny 设法实例化 x，但没有实例化 z。也许将其发布到他们的GitHub/Issues？

【讨论】：

验证者证明了y、x和z这样的存在，但是编译器无法处理最后一种情况。一般来说，人们应该期望验证者无法找到所有可能的证人，因此您可能必须自己提供他们。编译器处理这种情况的一种方法是在运行时枚举所有可能的整数序列，直到找到满足谓词的整数序列。这将终止，因为验证者已经证明存在这样的序列。但是，您会对运行时性能感到失望。
如果你真的认为编译器的任务是微不足道的，那么请提交一个拉取请求。