Using the verification rules in the notes, list all the con$-$

ditions that must be shown to be universally true in order to show

that the following proof outline is partially correct. Perform all sub$-$

stitutions. I.e$.$ state the condition using the substitution notation

$($when applicable$)$ and then restate it after doing the substitutions.

Assume state variables p and k are integers and that a is an array

of integers of length at least length M $,$ indexed from $0.$

$\{$A : M $>=0\}$

p$,$ k :$=0,0$

$\{$B : $0<=$ p $<=$ M $0<=$ k $<=$ M $($k $=$ p $$ a$($k$)=46)($i in $\{0,..$k$\}$ a$($i$)=46)\}$

while p $<$ M $$ k $=$ p do

$\{$C : $0<=$ p $<$ M $1<=$ k $<=$ M $$ k $=$ p $($i in $\{0,..$p$\}$ a$($i$)=46)\}$

if a$($p$)=46$ then

$\{$D : $0<=$ p $<$ M $1<=$ k $<=$ M $$ k $=$ p $($i in $\{0,..$p $+1\}$ a$($i$)=46)\}$

k :$=$ k $+1$

end if

$\{$E : $0<=$ p $+1<=$ M $0<=$ k $<=$ M $($k $=$ p $+1$ a$($k$)=46)($i in $\{0,..$k$\}$ a$($i$)=46)\}$

p :$=$ p $+1$

end while

$\{$F : $0<=$ k $<=$ M $($k $=$ M $$ a$($k$)=46)($i in $\{0,..$k$\}$ a$($i$)=46)\}$