I have the following program in Dafny:

predicate Q (x:int,y:int)
{
x == y
}

function F (j:int,s:seq<int>):int
requires 0 <= j < |s|-1
{
s[j+1] 
}

predicate Pi (i: nat, s:seq<int>)
   requires 1 <= i < |s|
{
Q(s[i-1],F(i-1,s))
}


predicate P (s:seq<int>)
{
forall i :: 1 <= i < |s| ==> Pi(i,s)
}

method checkforall (s:seq<int>) returns (b:bool)
requires |s| > 1
ensures b <==> P(s)
{
var j := 1;
b := true;
while j < |s| && Pi(j,s)
   invariant 0 <= j <= |s|
   invariant b <==> forall  i :: 1 <= i < j ==> Pi(i,s)  
   {
      j := j+1;
   }
if j < |s| 
   {
      b := false;
   }
}

method Main()
{
var s := [0,0,0,0,0];
var b := checkforall(s);
assert b;  
}

Dafny can prove the Main method, but it is unable to prove this:

method Main()
{
var s := [0,1,0,0,0];
var b := checkforall(s);
assert !b;  
}

Dafny needs the extra information assert !Pi(2,s), but I do not want to have to include this extra information. How can I do it?

I have the following program in Dafny:

predicate Q (x:int,y:int)
{
x == y
}

function F (j:int,s:seq<int>):int
requires 0 <= j < |s|-1
{
s[j+1] 
}

predicate Pi (i: nat, s:seq<int>)
   requires 1 <= i < |s|
{
Q(s[i-1],F(i-1,s))
}


predicate P (s:seq<int>)
{
forall i :: 1 <= i < |s| ==> Pi(i,s)
}

method checkforall (s:seq<int>) returns (b:bool)
requires |s| > 1
ensures b <==> P(s)
{
var j := 1;
b := true;
while j < |s| && Pi(j,s)
   invariant 0 <= j <= |s|
   invariant b <==> forall  i :: 1 <= i < j ==> Pi(i,s)  
   {
      j := j+1;
   }
if j < |s| 
   {
      b := false;
   }
}

method Main()
{
var s := [0,0,0,0,0];
var b := checkforall(s);
assert b;  
}

Dafny can prove the Main method, but it is unable to prove this:

method Main()
{
var s := [0,1,0,0,0];
var b := checkforall(s);
assert !b;  
}

Dafny needs the extra information assert !Pi(2,s), but I do not want to have to include this extra information. How can I do it?

• dafny

Share Improve this question Follow edited Nov 19, 2024 at 11:38 jonrsharpe 122k3030 gold badges268268 silver badges476476 bronze badges asked Nov 19, 2024 at 11:08 Montserrat HermoMontserrat Hermo 7133 bronze badges

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 0

I don't have a perfect explanation for you but basically for quantifiers Dafny/z3 seem to evaluate them lazily. However, if you use a function to calculate it instead then it actually does the work.

    predicate P'(s: seq<int>)
    {
        if |s| > 1 then Pi(1, s) && P'(s[1..]) else true
        
    }

    lemma PEqualP'(s: seq<int>)
        ensures P(s) <==> P'(s)
    {
        if |s| > 1 {
            if |s| == 2 {
                assert P(s) <==> Pi(1,s);
                if Pi(1,s) {
                    assert P(s) <==> Q(s[0],s[1]);
                    assert P(s) <==> P'(s);
                }else{
                    assert P(s) <==> false;
                    assert P(s) <==> P'(s);
                }
            }
            PEqualP'(s[1..]);
            if Pi(1,s) {
                assert Q(s[0],F(0,s));
                // assert P(s) <==> Q(s[0],F(0,s)) && P'(s[1..]);
                assert s == [s[0]] + s[1..];
                if !P'(s[1..]) {
                    var i :| 1 <= i < |s[1..]| && !Pi(i,s[1..]);
                    assert !Pi(i+1,s);
                    assert !P(s);
                } else{
                    assert forall i :: 1 <= i < |s[1..]| ==> Pi(i,s[1..]);
                    assert forall i :: 2 <= i < |s| ==> Pi(i, s) by {
                        forall i | 2 <= i < |s|
                            ensures Pi(i,s)
                        {
                            assert Pi(i-1,s[1..]);
                            assert Pi(i,s);
                        }
                    }
                }
                assert P(s) <==> P'(s);
            }else{
                assert P(s) <==> false;
                assert P(s) <==> P'(s);
            }
            assert P(s) <==> P'(s);
        }else{
            assert P(s) <==> true;
            assert P(s) <==> P'(s);
        }
    }

    method checkforall (s:seq<int>) returns (b:bool)
        requires |s| > 1
        ensures b == P(s)
        ensures b <==> P'(s)
    {
        var j := 1;
        b := true;
        while j < |s| && Pi(j,s)
        invariant 0 <= j <= |s|
        invariant b <==> forall  i :: 1 <= i < j ==> Pi(i,s)  
        {
            j := j+1;
        }
        if j < |s| 
        {
            b := false;
        }
        PEqualP'(s);
    }

    method Main(s: seq<int>)
    {
        var t := [0,0,0,0,0];
        var s := [0,2,0,0,0];
        var b := checkforall(s);
        assert !b;  
    }