CODEWITHSUNDEEP
dafny
jiplucap
jiplucap

Reputation: 164

Trick to check a forall with no triggers

In the first example the trick for checking a forall with no triggers works, but in the second the same idea does not work.

Example 1: This program is intentionally complicated to prevent Dafny generates triggers.

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 P (s:seq<int>)
{
forall i :: 1 <= i < |s| ==> Q(s[i-1],F(i-1,s))  
}

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

method Main()
{
var s := [0,0,0,0,0];
var b := checkforall(s);
assert b;  //Verified
}
´´´
The second example will be in a second post-

Upvotes: 1

Views: 20

Answers (0)

Related Questions