Loop invariants

Feb 25, 2013 at 12:23 AM
Hi Rustan ---

Since your email about how to use ghost methods, parallel and the advice to put assumptions as requirements rather than antecedents, I have made enormous progress. Thanks!

I now seem to be stuck with two much more mundane issues; they're labelled 1 and 2 in the code further below. (It won't compile without its other definitions, but I'll send them out-of-band to avoid swamping this post.)

My strategy at this point is to develop the loop from the outside in. Here are my two problems:

1) This inner assert does not seem to be flagged as violated, though it should be: it need appeals to the ghost methods about sequences and so on, and (surely?) it needs to know something about m. I have experimented by writing ridiculous things there, and unless they are -propositionally- ridiculous, no error seems to be flagged.

But I need to have that assertion flagged as violated in order to figure out which ghost methods it needs.

2) The errors that -are- flagged are that the postcondition might not hold (of course), but also that the final assert (below the comment) is invalid... but it is just part of the invariant, verbatim.

I put these here in case the postcondition violations might have been stopping Dafny from looking inside the loop and spotting violation 1 above. But unless I can get it to accept those assertions, I'm stymied here too.

Could you give some advice?

Thanks!

----- Code: its first line is number 212.
method findLUS (bs: seq<int>) returns (cs: seq<int>)
ensures isUpsequence(bs,cs);
ensures forall ds:: isUpsequence(bs,ds) ==> |ds|<=|cs|; {

var n,l:= 0,0;
var luss: seq<seq<int>>:= [[]];
while (n<|bs|) 
    invariant 0<=n<=|bs|;
    invariant |luss|==l+1;
    invariant forall j,lus:: 0<=j<=l && lus==luss[j] ==> |lus|==j && isLowestUpsequence(bs[..n],lus); 
    invariant forall ds:: isUpsequence(bs[..n],ds) ==> |ds|<=l;

{
    // Binary search does this.
    var m: int;
    assume 1<=m<=l+1;
    // assume forall p:: 1<=p<m ==> Last(luss[p])<bs[n];
    // assume forall q:: m<=q<l+1 ==> bs[n]<=Last(luss[q]);

    /** 1 **/
    assert forall p:: 1<=p<m ==> isLowestUpsequence(bs[..n+1],luss[p]);

    n:= n+1;

    assume |luss|==l+1;
    assume forall j,lus:: 0<=j<=l && lus==luss[j] ==> |lus|==j && isLowestUpsequence(bs[..n],lus); 
    assume forall ds:: isUpsequence(bs[..n],ds) ==> |ds|<=l;
}
assert |luss|==l+1;
assert forall j,lus:: 0<=j<=l && lus==luss[j] ==> |lus|==j && isLowestUpsequence(bs,lus); 
/** 2 **/
assert forall ds:: isUpsequence(bs,ds) ==> |ds|<=l;
}

----- Dafny output:

bash-3.2$ dafny Sequences3.dfy
Dafny program verifier version 1.6.0.00123, Copyright (c) 2003-2013, Microsoft.
Sequences3.dfy(214,58): Error BP5003: A postcondition might not hold on this return path.
Sequences3.dfy(213,10): Related location: This is the postcondition that might not hold.
Sequences3.dfy(61,27): Related location: Related location
Sequences3.dfy(14,3): Related location: Related location
Execution trace:
(0,0): anon0
Sequences3.dfy(218,2): anon42_LoopHead
(0,0): anon42_LoopBody
Sequences3.dfy(218,2): anon43_Else
(0,0): anon14
(0,0): anon50_Then
(0,0): anon32
(0,0): anon59_Then
(0,0): anon60_Then
(0,0): anon61_Then
(0,0): anon62_Then
(0,0): anon39
(0,0): anon63_Then
(0,0): anon41
Sequences3.dfy(214,58): Error BP5003: A postcondition might not hold on this return path.
Sequences3.dfy(213,10): Related location: This is the postcondition that might not hold.
Sequences3.dfy(61,3): Related location: Related location
Sequences3.dfy(7,30): Related location: Related location
Execution trace:
(0,0): anon0
Sequences3.dfy(218,2): anon42_LoopHead
(0,0): anon42_LoopBody
Sequences3.dfy(218,2): anon43_Else
(0,0): anon14
(0,0): anon50_Then
(0,0): anon32
(0,0): anon59_Then
(0,0): anon60_Then
(0,0): anon61_Then
(0,0): anon62_Then
(0,0): anon39
(0,0): anon63_Then
(0,0): anon41
Sequences3.dfy(214,58): Error BP5003: A postcondition might not hold on this return path.
Sequences3.dfy(213,10): Related location: This is the postcondition that might not hold.
Sequences3.dfy(61,3): Related location: Related location
Sequences3.dfy(6,30): Related location: Related location
Execution trace:
(0,0): anon0
Sequences3.dfy(218,2): anon42_LoopHead
(0,0): anon42_LoopBody
Sequences3.dfy(218,2): anon43_Else
(0,0): anon14
(0,0): anon50_Then
(0,0): anon32
(0,0): anon59_Then
(0,0): anon60_Then
(0,0): anon61_Then
(0,0): anon62_Then
(0,0): anon39
(0,0): anon63_Then
(0,0): anon41
Sequences3.dfy(214,58): Error BP5003: A postcondition might not hold on this return path.
Sequences3.dfy(213,10): Related location: This is the postcondition that might not hold.
Sequences3.dfy(61,3): Related location: Related location
Sequences3.dfy(5,30): Related location: Related location
Execution trace:
(0,0): anon0
Sequences3.dfy(218,2): anon42_LoopHead
(0,0): anon42_LoopBody
Sequences3.dfy(218,2): anon43_Else
(0,0): anon14
(0,0): anon50_Then
(0,0): anon32
(0,0): anon59_Then
(0,0): anon60_Then
(0,0): anon61_Then
(0,0): anon62_Then
(0,0): anon39
(0,0): anon63_Then
(0,0): anon41
Sequences3.dfy(243,9): Error: assertion violation
Execution trace:
(0,0): anon0
Sequences3.dfy(218,2): anon42_LoopHead
(0,0): anon42_LoopBody
Sequences3.dfy(218,2): anon43_Else
(0,0): anon14
(0,0): anon50_Then
(0,0): anon32
(0,0): anon59_Then
(0,0): anon60_Then
(0,0): anon61_Then
(0,0): anon62_Then
(0,0): anon39
(0,0): anon63_Then
(0,0): anon41
Dafny program verifier finished with 24 verified, 5 errors

real 0m3.392s
user 0m3.368s
sys 0m0.060s
bash-3.2$