CODEWITHSUNDEEP
predicateassertiondafnyexplicit
Montserrat Hermo
Montserrat Hermo

Reputation: 71

One-by-one assertions versus single predicates in Dafny. Any advice?

I have a (not small) module in Dafny and at some point the following can be asserted.

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));

Obviously, I prefer to use a predicate to do this and I have defined:

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)))
}

However, if I replace the first piece of code with

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

assert wellDefinedSeq(seq5, envir);

Dafny is unable to assert the predicate. Any idea why this happens?

Upvotes: 0

Views: 51

Answers (1)

Hath995
Hath995

Reputation: 1300

This seems to work fine. Probably, there is some requirement for your functions that are not being met. You'll probably need to post more of your code to really get an answer.


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));

    }
}

Upvotes: 0

Related Questions