Dafny 中的一对一断言与单个谓词。有什么建议吗？

Question

我在 Dafny 中有一个（不小的）模块，在某些时候可以断言以下内容。

var  seq5:= [R1, R2, R3, R3, R3];    

assert wellDefinedGRequirement(seq5[0], envir);
assert wellDefinedGRequirement(seq5[1], nextEnv(0, seq5, envir));
assert wellDefinedGRequirement(seq5[2], nextEnv(1, seq5, envir));
assert wellDefinedGRequirement(seq5[3], nextEnv(2, seq5, envir));
assert wellDefinedGRequirement(seq5[4], nextEnv(3, seq5, envir));

显然，我更喜欢使用谓词来做到这一点，并且我已经定义了：

predicate wellDefinedSeq(seqR: seq<GRequirement>, m: Env)
requires |seqR| > 0
{
  wellDefinedGRequirement(seqR[0], m) &&
  (forall i:: 1 <= i < |seqR| ==>  wellDefinedGRequirement(seqR[i], nextEnv(i-1, seqR, m)))
}

但是，如果我将第一段代码替换为

var  seq5:= [R1, R2, R3, R3, R3]; 

assert wellDefinedSeq(seq5, envir);

Dafny 无法断言谓词。知道为什么会发生这种情况吗？

Answer 1

这似乎工作正常。可能您的功能有一些要求没有得到满足。您可能需要发布更多代码才能真正得到答案。

module SO3 {
    
    predicate wellDefinedGRequirement<T, E>(elem: T, envir: E)

    function nextEnv<T, E>(index: int, xs: seq<T>, envir: E): E
       
    predicate wellDefinedSeq<T,E>(seqR: seq<T>, m: E)
        requires |seqR| > 0
    {
        wellDefinedGRequirement(seqR[0], m) &&
        (forall i:: 1 <= i < |seqR| ==>  wellDefinedGRequirement(seqR[i], nextEnv(i-1, seqR, m)))
    }
    method test<T, E>(seq5: seq<T>, R1: T, R2: T, R3: T, envir: E) 
        requires seq5 == [R1, R2, R3, R3, R3]
        requires wellDefinedGRequirement(seq5[0], envir);
        requires wellDefinedGRequirement(seq5[1], nextEnv(0, seq5, envir));
        requires wellDefinedGRequirement(seq5[2], nextEnv(1, seq5, envir));
        requires wellDefinedGRequirement(seq5[3], nextEnv(2, seq5, envir));
        requires wellDefinedGRequirement(seq5[4], nextEnv(3, seq5, envir));
    {
        assert wellDefinedGRequirement(seq5[0], envir);
        assert wellDefinedGRequirement(seq5[1], nextEnv(0, seq5, envir));
        assert wellDefinedGRequirement(seq5[2], nextEnv(1, seq5, envir));
        assert wellDefinedGRequirement(seq5[3], nextEnv(2, seq5, envir));
        assert wellDefinedGRequirement(seq5[4], nextEnv(3, seq5, envir));

        assert wellDefinedSeq(seq5, envir);
    }

    method test2<T, E>(seq5: seq<T>, R1: T, R2: T, R3: T, envir: E) 
        requires seq5 == [R1, R2, R3, R3, R3]
        requires wellDefinedSeq(seq5, envir)
    {
        assert wellDefinedGRequirement(seq5[0], envir);
        assert wellDefinedGRequirement(seq5[1], nextEnv(0, seq5, envir));
        assert wellDefinedGRequirement(seq5[2], nextEnv(1, seq5, envir));
        assert wellDefinedGRequirement(seq5[3], nextEnv(2, seq5, envir));
        assert wellDefinedGRequirement(seq5[4], nextEnv(3, seq5, envir));

    }
}