method Filter$($a:seq, b:set$)$ returns$($c:set$)$

ensures forall j :: $0<=$ j $<|$a$|==>$ if $($a$[$j$]$ in b$)$ then $($a$[$j$]$ in c$)$

else $!($a$[$j$]$ in c$)$

$\{$

c :$=\{\}$;

var i : int :$=0$;

while i $<|$a$|$

invariant $0<=$ i $<=|$a$|$

invariant forall j :: $0<=$ j $<$ i $==>$ if $($a$[$j$]$ in b$)$ then $($a$[$j$]$ in c$)$ else $!($a$[$j$]$ in c$)$

$\{$

if $($a$[$i$]$ in b$)$

$\{$

c :$=$ c $+\{$a$[$i$]\}$;

$\}$

i :$=$ i $+1$;

$\}$

$\}$

for my code why ype errors detected in filter.dfy

z$5421798$@vx$19$:~$/$seng$2011/$exam$ seng$2011$ dafny verify filter.dfy

filter.dfy$(73,14)$: Error: this invariant could not be proved to be maintained by the loop

Related message: loop invariant violation

$|$

$73|$ invariant forall j :: $0<=$ j $<$ i $==>$ if $($a$[$j$]$ in b$)$ then $($a$[$j$]$ in c$)$ else $!($a$[$j$]$ in c$)$

$|^^^^^^$

Dafny program verifier finished with $1$ verified, $1$ err

why is my invariant weak