dafny - Invariant set may vary -

a method copies negative elements of array of integers array has property set of elements in result subset of elements in original array, stays same during copy.

the problem in code below that, write in result array, dafny somehow forgets original set unchanged. how fix this?

method copy_neg (a: array<int>, b: array<int>)   requires != null && b != null && != b   requires a.length == b.length   modifies b {   var := 0;   var r := 0;   ghost var sa := set j | 0 <= j < a.length :: a[j];   while < a.length     invariant 0 <= r <= <= a.length     invariant sa == set j | 0 <= j < a.length :: a[j]   {     if a[i] < 0 {       assert sa == set j | 0 <= j < a.length :: a[j]; // ok       b[r] := a[i];       assert sa == set j | 0 <= j < a.length :: a[j]; // ko!       r := r + 1;     }     := + 1;   } } 

edit

following james wilcox's answer, replacing inclusions of sets predicates on sequences works best.

here complete specification (for array distinct elements). post-condition has detailed bit in loop invariant , dumb assert remains in middle of loop, ghost variables gone, great.

method copy_neg (a: array<int>, b: array<int>)   returns (r: nat)   requires != null && b != null && != b   requires a.length <= b.length   modifies b   ensures 0 <= r <= a.length   ensures forall x | x in a[..] :: x < 0 <==> x in b[..r] {   r := 0;   var := 0;   while < a.length     invariant 0 <= r <= <= a.length     invariant forall x | x in b[..r] :: x < 0     invariant forall x | x in a[..i] && x < 0 :: x in b[..r]   {     if a[i] < 0 {       b[r] := a[i];       assert forall x | x in b[..r] :: x < 0;       r := r + 1;     }     := + 1;   } } 

this indeed confusing. explain why dafny has trouble proving below, first let me give few ways make go through.

first workaround

one way make proof go through insert following forall statement after line b[r] := a[i];.

forall x | x in sa   ensures x in set j | 0 <= j < a.length :: a[j] {   var j :| 0 <= j < a.length && x == old(a[j]);   assert x == a[j]; } 

the forall statement proof sa <= set j | 0 <= j < a.length :: a[j]. come why works below.

second workaround

in general, when reasoning arrays in dafny, best use a[..] syntax convert array mathematical sequence, , work sequence. if need work set of elements, can use set x | x in a[..], , have better time if use set j | 0 <= j < a.length :: a[j].

systematically replacing set j | 0 <= j < a.length :: a[j] set x | x in a[..] causes program verify.

third solution

popping level specifying method, seems don't need mention set of elements. instead, can away saying "every element of b element of a". or, more formally forall x | x in b[..] :: x in a[..]. not quite valid postcondition method, because method may not fill out of b. since i'm not sure other constraints are, i'll leave you.

explanations

dafny's sets elements of type a translated boogie maps [a]bool, element maps true iff in set. comprehensions such set j | 0 <= j < a.length :: a[j] translated boogie maps definition involves existential quantifier. particular comprehension translates map maps x to

exists j | 0 <= j < a.length :: x == read($heap, a, indexfield(j)) 

where read expression boogie translation of a[j], which, in particular, makes heap explicit.

so, prove element in set defined comprehension, z3 needs prove existential quantifier, hard. z3 uses triggers prove such quantifiers, , dafny tells z3 use trigger read($heap, a, indexfield(j)) when trying prove quantifier. turns out not great trigger choice, because mentions current value of heap. thus, when heap changes (ie, after updating b[r]), trigger may not fire, , failing proof.

dafny lets customize trigger uses set comprehensions using {:trigger} attribute. unfortunately, there no great choice of trigger @ dafny level. however, reasonable trigger program @ boogie/z3 level indexfield(j) (though bad trigger such expressions in general, since overly general). z3 infer trigger if dafny doesn't tell otherwise. can dafny out of way saying {:autotriggers false}, this

invariant sa == set j {:autotriggers false} | 0 <= j < a.length :: a[j] 

this solution unsatisfying , requires detailed knowledge of dafny's internals. we've understood it, can understand other workarounds proposed.

for first workaround, proof goes through because forall statement mentions a[j], trigger. causes z3 prove existential.

for second workaround, have simplified set comprehension expression no longer introduces existential quantifier. instead comprehension set x | x in a[..], translated map maps x to

x in a[..] 

(ignoring details of how a[..] translated). means z3 never has prove existential, otherwise similar proof goes through.

the third solution works similar reasons, since uses no comprehensions , no problematic existential quantifiers/