exercise $6($solution in ex$6.$dfy$)7$ marks. A bad neighbour in an array is a neighbouring pair of elements that sum to a negative integer. In this exercise, the first and last elements of an array $($of length at least $2)$ are considered neighbours. For example, the arrays $[0,-1],[0,42,-1]$ and $[5,6,-7,6]$ each contains at least one bad neighbour. The arrays $[42],[2,3,-1]$ and $[2,-1,2,-1]$ do not contain any bad neighbours. Create a file ex$6.$dfy that contains a Dafny predicate with signature: predicate badneighbour$($a: array$)$ which is true if the given input array contains at least one bad neighbour and is false otherwise. There are no restrictions on the size of the array. Validate that your predicate works correctly by writing a validator method called ValBadNeighbour. Submit the file ex$6.$dfy$,$ which should contain the predicate badneighbour and the method ValBadNeighbour. Notice the predicate name $($badneighbour$)$ consists of lower$-$case letters only. Your Dafny programs will be partly auto$-$marked so it is important that the names of the methods and the predicate, and the filenames, are spelt correctly and are case$-$correct.