Consider the following IMP program:

i :$=0$;

j :$=$ len$($arr$)-1$;

while i $<=$ j do

if arr$[$i$]<=$ arr$[0]$ then

i :$=$ i $+1$

else

tmp :$=$ arr$[$i$]$;

arr$[$i$]$ :$=$ arr$[$j$]$;

arr$[$j$]$ :$=$ tmp;

j :$=$ j $-1$

Givenanon$-$emptyarrayofintegersarr$($withindexes$0$throughlen$($arr$)-1),$theprogramattempts to partition arr such that all elements lesser than or equal to its first element appear before all elements greater than its first element.

Come up with assertions P $($the loop invariant$)$ and Q $($the loop postcondition$),$ in terms of i$,$ j$,$ and arr, that can be used to demonstrate partial correctness of the program. Briefly explain how P can be used to imply Q$.$