method BadNbr$($a: array$)$ returns $($bn: int$)$

ensures a$.$Length $<2==>$ bn $==-1$

ensures bn $>=0==>$ bn $<$ a$.$Length

ensures bn $==-1==>$ forall i :: $0<=$ i $<$ a$.$Length $==>$ a$[$i$]+$ a$[($i $+1)\%$ a$.$Length$]>=0\{$:trigger a$[$i$],$ a$[($i $+1)\%$ a$.$Length$]\}$

$\{$

$//$ Base case: if the array length is less than $2,$ no bad neighbours possible.

if a$.$Length $<2\{$

return $-1$;

$\}$

var n :$=$ a$.$Length;

$//$ Check the wrap$-$around pair $($last and first elements$)$

if a$[$n $-1]+$ a$[0]<0\{$

return $0$;

$\}$

$//$ Check for bad neighbours in consecutive pairs

var i :$=0$;

while i $<$ n $-1$

invariant $0<=$ i $<=$ n $-1$

invariant forall j :: $0<=$ j $<$ i $==>$ a$[$j$]+$ a$[$j $+1]>=0$

decreases n $-$ i

$\{$

if a$[$i$]+$ a$[$i $+1]<0\{$

return i $+1$;

$\}$

i :$=$ i $+1$;

$\}$

$//$ Final check to ensure all pairs are non$-$negative before returning $-1$

assert forall i :: $0<=$ i $<$ n $==>$ a$[$i$]+$ a$[($i $+1)\%$ n$]>=0\{$:trigger a$[$i$],$ a$[($i $+1)\%$ n$]\}$;

return $-1$;

$\}$

method TestBadNbr$()$

$\{$

$//$ Test case $1$: Empty array

var arr$1$ :$=$ new int$[0]$;

var res$1$ :$=$ BadNbr$($arr$1)$;

assert res$1==-1$;

$//$ Test case $2$: Array with one element

var arr$2$ :$=$ new int$[1]$;

arr$2[0]$ :$=5$;

var res$2$ :$=$ BadNbr$($arr$2)$;

assert res$2==-1$;

$//$ Test case $3$: Array with two elements where sum is negative

var arr$3$ :$=$ new int$[2]$;

arr$3[0]$ :$=1$;

arr$3[1]$ :$=-2$;

var res$3$ :$=$ BadNbr$($arr$3)$;

assert res$3==1$;

$//$ Test case $4$: Array with three elements and a bad neighbour pair

var arr$4$ :$=$ new int$[3]$;

arr$4[0]$ :$=3$;

arr$4[1]$ :$=-4$;

arr$4[2]$ :$=1$;

var res$4$ :$=$ BadNbr$($arr$4)$;

assert res$4==1$;

$//$ Test case $5$: Array with four elements and a wrap$-$around bad neighbour pair

var arr$5$ :$=$ new int$[4]$;

arr$5[0]$ :$=2$;

arr$5[1]$ :$=-1$;

arr$5[2]$ :$=3$;

arr$5[3]$ :$=-4$;

var res$5$ :$=$ BadNbr$($arr$5)$;

assert res$5==0$;

$//$ Test case $6$: No bad neighbour

var arr$6$ :$=$ new int$[3]$;

arr$6[0]$ :$=3$;

arr$6[1]$ :$=2$;

arr$6[2]$ :$=1$;

var res$6$ :$=$ BadNbr$($arr$6)$;

assert res$6==-1$;

$//$ Test case $7$: Only wrap$-$around is a bad neighbour

var arr$7$ :$=$ new int$[4]$;

arr$7[0]$ :$=-1$;

arr$7[1]$ :$=2$;

arr$7[2]$ :$=3$;

arr$7[3]$ :$=-4$;

var res$7$ :$=$ BadNbr$($arr$7)$;

assert res$7==0$;

$\}$