Dafny: Verify using invariant and decreases

Jan 23, 2016 at 10:00 AM
Edited Jan 23, 2016 at 10:05 AM
I am trying to get the below program verified.
I mean only to change invariant and decreases statements.
How can i do this?? I have tried several possibilities with no success.
    method Main() {
     var a:int := 0;
     var b:int := -1;
     var c:int := 0;
     var i:int := 100;
     while (a!=b)
     invariant 0<=c<=i
     decreases i-c
     {
         b := a;
                 c := c + 1;
         if (c < i) {
                  a := a + 1;
         }
     }
    print "Eureka";
}
Jan 23, 2016 at 9:49 PM
It would be interesting to know some of the other things you tried.

It seems that Dafny can't work out that (b==a <==> c==i), so you have to tell it.
method Main() {
     var a:int := 0;
     var b:int := -1;
     var c:int := 0;
     var i:int := 100;
     
     while (a!=b)
      invariant 0<=c<=i
      invariant c == i ==> b == a;
      decreases i-c
     {
         b := a;
         c := c + 1;
         if (c < i) {
              a := a + 1;
         }
     }
     print "Eureka";
}
Marked as answer by piyushroshan on 1/23/2016 at 7:07 PM
Jan 24, 2016 at 3:56 AM
Edited Jan 24, 2016 at 5:14 AM
What about the following then:
I tried adding:
 invariant b == a ==> l.state == true;
 invariant b < a ==> l.state == false;
class Lock {
    var state:bool;
 
    constructor init()
    modifies this;
    ensures state == false;
    {
        state := false;
    }
 

    method acquireLock()
    modifies this;
    ensures state == true;
    {
        state := !state;
    }
 
    method releaseLock()
    modifies this;
    ensures state == false;
    {
        state := !state;
    }
}

method Main() {
     var a:int := 0;
     var b:int := -1;
     var c:int := 0;
     var l:Lock := new Lock.init();
     var i:int := 100;
     while (a!=b)
     invariant 0<=c<=i
     invariant c == i ==> b == a;
     decreases i-c;
     {
         b := a;
         c := c+1;
         l.acquireLock();
         if(c < i){
             a := a+1;
             l.releaseLock();
         }
     }
    l.releaseLock();
    print "Eureka";
}
Jan 24, 2016 at 9:20 AM
Your Lock class has a strange definition, and the method postconditions do not verify. I guessed a definition which does verify...

Roughly, the thing about loop invariants is that the loop invariant of the previous iteration has to be strong enough that you can prove

(loop invariant previous iteration) and (body of loop) ==> loop invariant
class Lock {
    var state:bool;
 
    constructor init()
    modifies this;
    ensures !state;
    {
        state := false;
    }
 

    method acquireLock()
    modifies this;
    ensures state
    {
        state := true;
    }
 
    method releaseLock()
    modifies this;
    ensures !state
    {
        state := false;
    }
}

method Main() {
     var a:int := 0;
     var b:int := -1;
     var c:int := 0;
     var l:Lock := new Lock.init();
     var i:int := 100;
     while (a!=b)
     invariant 0<=c<=i
     invariant c < i ==> b + 1 == a && !l.state;
     invariant c == i ==> b == a && l.state;
     decreases i-c;
     {
         b := a;
         c := c+1;
         l.acquireLock();
         if(c < i){
             a := a+1;
             l.releaseLock();
         }
     }
    l.releaseLock();
    print "Eureka";
}