Below we give, in Java syntax, the sumn method which computes the sum of the n natural numbers

from $1$ to n$.$ For example, sumn$(0)==0,$ sumn$(1)==1,$ sumn$(2)==3,$ and sumn$(6)==21.$

$//$ P r e c o n d i t i o n : n $>=0$

int sumn $($ int n $)\{$

int i $=0,$ t $=0$ ;

while $($ i $<$ n $)\{$

i $=$ i $+1$ ;

t $=$ t $+$ i ;

$\}$

return t ;

$\}$

$//$ P o s t c o n d i t i o n : t $=$ n $*($ n $+1)/2$

a$)$ Find a suitable loop invariant. $(2$ pt$.)$

b$)$ Show that the invariant holds before the loop $($base case$).(1$ pt$.)$

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$).(3$ pts$.)$

d$)$ Show that the loop exit condition and the loop invariant imply the postcondition t $=$ n$($n$+1)/2.$

$(2$ pts$.)$

e$)$ Find a suitable decrementing function. Show that the function is non$-$negative before loop starts,

that it decreases at each iteration and that when it reaches $0$ the loop is exited. $(2$ pts$.)$

f$)$ Implement the sum of natural numbers in Dafny.