CODEWITHSUNDEEP
iterationbreakdafny
david streader
david streader

Reputation: 589

What does Dafny know about loops with a break?

I am used to loops

while Grd
invariant Inv
{ ..}
assert Inv && !Grd;

with out any break Dafny knows that Inv && ! Grd is true but: Dafny does not check the loop invariant after a break; command. Hence

method tester(s:seq<int>) returns (r:int) 
ensures r <= 0
{   var i:nat := |s|;
    r := 0;
    while (i > 0)
       decreases i
       invariant r == 0;
    {   i := i -1;
        if s[i]< 0  { r:= s[i]; break;}        
    }    
   // assert r == 0; // invariant dose not hold
}

method Main() {
    var x:int := tester([1,-9,0]);
    print x,"\n";
}

Clearly Dafny understands that the invariant no longer holds. Could anyone tell me what dafny actually knows.

Upvotes: 2

Views: 682

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

If there are break statements, the condition after the loop is the disjunction of Inv && !Grd and the conditions that hold at the respective break statements.

Here's a more formal answer:

In the absence of any abrupt exits (like break) from a loop, the familiar way to prove the Hoare triple

{{ P }}
while Grd
  invariant Inv
{
  Body
}
{{ Q }}

is to prove the following three conditions (I'm ignore termination):

  1. Check that the loop invariant holds on entry to the loop:
P ==> Inv
  1. Check that the loop invariant is maintained by the loop body:
{{ Inv && Grd }}
Body
{{ Inv }}
  1. Check that the invariant and negated guard prove Q:
Inv && !Grd ==> Q

Let me rephrase conditions 1 and 2. To do that, I will start by rewriting the while loop into a repeat-forever loop with breaks:

loop
  invariant Inv
{
  if !Grd {
    break;
  }
  Body
}

(In other words, I'm using loop as while true.) Proof obligation 1 above can now be rephrased as proving

{{ Inv }}
if !Grd {
  break;
}
Body
{{ Inv }}

where you don't have to prove anything further along any path that reaches a break. Proof obligation 2 can be rephrased in a sort of dual way:

{{ Inv }}
if !Grd {
  break;
}
Body
{{ break: Q }}

by which I mean you don't have to prove anything if you reach the end of ...Body, but you do have to prove Q at any break.

What I just said also applies when Body contains other break statements. That's how Dafny treats loops (that is, condition 0 plus the rephrased conditions 1 and 2, plus termination checking).

Upvotes: 5

Related Questions