CODEWITHSUNDEEP
predicatedafnyforall
Montserrat Hermo
Montserrat Hermo

Reputation: 71

Problem with an assertion in Dafny that uses a universal quantifier

I asked a question about "forall predicates" in Dafny but following the advice of an answer I didn't get what I wanted.

The problem is the following: I have an "assert for all i :: 0 <= i < |s| ==> P(i,s)" where s is a finite sequence with assigned values ​​and P a predicate defined in my code. Dafny can't verify the assertion (probably due to the triggers it uses) but it can verify each "assertion P(0,s)" "assertion P(1,s)" ..."assertion P(|s |-1, s)". Since s can be very large, writing all asserts is not a suitable solution. I would like to do this systematically for many sequences, please can someone tell me if there is a way to help Dafny do this? Is it possible to force Dafny with triggers to check a finite-domain forall?

Upvotes: 0

Views: 89

Answers (1)

Divyanshu Ranjan
Divyanshu Ranjan

Reputation: 1665

Since individually P(i, s) forall i such that 0 <= i < |s| verifies.

One advise would be write following and see if it verifies

   forall i | 0 <= i < |s| ensures P(i, s) {}
   assert forall i :: 0 <= i < |s| ==> P(i, s);

An example to demonstrate above is following

predicate NotTrue(p: nat)
{ 
    if p == 0 then false
    else NotTrue(p-1)
}

ghost predicate Q(i: nat, s: seq<nat>)
    requires 0 <= i < |s|
{
    forall k : nat :: 0 <= k <= s[i] ==> !NotTrue(k)
}

lemma M(s: seq<nat>)
   requires |s| > 0
   requires forall i :: 0 <= i < |s| ==> s[i] <= 2
{
   assert Q(0, s);
   assert Q(|s|-1, s);
   forall i | 0 <= i < |s| ensures Q(i, s) {}
   assert forall i :: 0 <= i < |s| ==> Q(i, s);
}

In absence of line forall i | 0 <= i < |s| ensures Q(i, s) {}, this assert forall i :: 0 <= i < |s| ==> Q(i, s); doesn't verify.

Upvotes: 1

Related Questions