do-while loops

Sep 29, 2016 at 5:37 PM
Edited Sep 29, 2016 at 5:40 PM
Is there a good way to deal with loops that will execute at least once?

For example, in the following, the verifier complains that m might not decrease in the outer loop.
method divideWithRemainder(x : int, y : int) returns ( p : int, m : int ) 
    requires y > 0 
    requires x >= 0
    ensures  p*y + m == x
    ensures 0 <= m
    ensures m < y
{
    p := 0 ;
    m := x ;
    // Use the first two conjucts of the postcondition as the invariant
    while( m >= y ) 
    invariant 0 <= m  // From postcondition
    invariant p * y + m == x // From postcondition
    decreases m 
    {
        var q := 1 ;
        assert m >= q * y ;
        while( m >= q * y )
            invariant 0 <= m 
            invariant p * y + m == x
            decreases m
        {
            p := p + q ;
            m := m - q * y ;
            q := 2*q ;
        }
    }
}
I tried to hint that the inner while loop would be executed at least once by using an assert.

Of course I can just repeat the loop body before the loop, but this seems inelegant.

Interestingly, if I delete q := 2*q, it verifies.

As a feature request, how about this
        label lp:
            invariant 0 <= m 
            invariant p*y + m == x
            decreases m
        {
            p := p + q ;
            m := m - q*y ;
            q := 2*q ;
            if( m < q*y ) goto lp ;
        }
Sep 30, 2016 at 2:26 AM
The answer is embarrassingly simple:
        label lp: while( true )
            invariant 0 <= m 
            invariant p*y + m == x
            decreases m
        {
            p := p + q ;
            m := m - q*y ;
            q := 2*q ;
            if( m >= q*y ) break lp ;
        }
I still like the goto idea, since it's useful for certain other things. (Even better than "goto lp" is "call lp", with the understanding that tail calls optimize to gotos.)
Oct 1, 2016 at 11:25 AM
You can use implication in loop invariants as a way to distinguish the behaviour of different loop iterations. In this case we need to distinguish that the first loop iteration is always executed but subsequent ones may or may not be executed. A ghost variable is used to track the initial value of m. Thus one can prove correctness of your original loop.
method divideWithRemainder(x : int, y : int) returns ( p : int, m : int ) 
    requires y > 0 
    requires x >= 0
    ensures  p*y + m == x
    ensures 0 <= m
    ensures m < y
{
    p := 0 ;
    m := x ;
    // Use the first two conjucts of the postcondition as the invariant
    while( m >= y ) 
    invariant 0 <= m  // From postcondition
    invariant p * y + m == x // From postcondition
    decreases m 
    {
        ghost var m' := m;
        var q := 1 ;
        assert m >= q * y ;
        while( m >= q * y )
            invariant q*y > 0
            invariant m == m' ==> m >= q * y
            invariant m <= m'
            invariant 0 <= m 
            invariant p * y + m == x
            decreases m
        {
            p := p + q ;
            m := m - q * y ;
            q := 2*q ;
        }
        assert m < m';
    }
}
Oct 2, 2016 at 4:19 PM
Thanks, that works nicely. It also works without the two assert commands.

I still prefer the use of break, since it didn't require any new variables or invariants.
Coordinator
Nov 29, 2016 at 12:18 AM
Just as in Java, you can use break; (without a label name) if you want to break out of the closest enclosing loop. Unlike in Java, you can also repeat the break keyword in order to break out of some other enclosing loop. For example, if you have an outer loop and an inner loop and want to break out of both loops from inside the inner loop, then you can either label the outer loop and list the label in the break statement:
label Outer:
while ...
{
  ...
  while ...
  {
    ...
    break Outer;
    ...
  }
  ...
}
or you can use a break break; statement, which breaks out of two levels of loops:
while ...
{
  ...
  while ...
  {
    ...
    break break;
    ...
  }
  ...
}
Rustan