This program is a smarter version of linear search. The program tests whether the array contains 0. It stops as soon as it finds a 0 (where the 'naive' of linear search would here simply continue till the end of the array).{= 0<=N =} { n=0 ; b=F ; inv (! i: 0<=i /\ i < n : ~(a#i=0)) /\ 0<=n /\ n<=N /\ (b ==> (a#n=0)) /\ (b ==> n < N) while (~b /\ ~(n=N)) if (a#n=0) b=T else n=n+1 ; } {= b = (? i: 0<=i /\ i < N : a#i=0) =}