Problem $4(17$ pts$.)$: Array of differences

Below is the pseudocode for creating an array containing elements each of which is the difference between two adjacent elements of the input array:a$)$ Find a suitable loop invariant. $(2$ pts$.)$b$)$ Show that the invariant holds before the loop $($base case$).(2$ pts$.)$c$)$ Show by induction that if the invariant holds after k$-$th iteration, and execution takes a k$+1-$st iteration, the invariant still holds $($inductive step$).(5$ pts$.)$d$)$ Show that the loop exit condition and the loop invariant imply the postcondition dif f s$.$Length $=$ arr.Length $-1^^$AA k$,$ s$.$t k $$ diff s$.$Length, diffs $[$k$]=$arr$[$k$+1]-$arr$[$k$].(3$ pts$.)$e$)$ Find a suitable decrementing function. Show that the function is not negative before loop starts, that it decreases at each iteration and that when it reaches $0$ the loop is exited. $(3$ pts$.)$f$)$ Implement the array of differences in Dafny. $(2$ pts$.,$ autograded$)$g$)$ Extra credit $(3$ pts$.)$ Implement difference in Dafny using sequences instead of arrays.