$(****$ Exercise: Two Loops $*)$

$(******$ Exercise: $3$ stars, standard $($two$\_$loops$)$

Here is a pretty inefficient way of adding $3$ numbers:

X :$=0$;

Y :$=0$;

Z :$=$ c;

while X $<>$ a do

X :$=$ X $+1$;

Z :$=$ Z $+1$

end;

while Y $<>$ b do

Y :$=$ Y $+1$;

Z :$=$ Z $+1$

end

Show that it does what it should by completing the

following decorated program.

$*)$

Definition two$\_$loops$\_$dec $($a b c : nat$)$ : decorated :$=$

$<\{$

$\{\{$ True $\}\}->>$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$

X :$=0$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$;

Y :$=0$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$;

Z :$=$ c

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$;

while X $<>$ a do

$\{\{$ FILL$\_$IN$\_$HERE $\}\}->>$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$

X :$=$ X $+1$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$;

Z :$=$ Z $+1$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$

end

$\{\{$ FILL$\_$IN$\_$HERE $\}\}->>$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$;

while Y $<>$ b do

$\{\{$ FILL$\_$IN$\_$HERE $\}\}->>$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$

Y :$=$ Y $+1$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$;

Z :$=$ Z $+1$

$\{\{$ FILL$\_$IN$\_$HERE $\}\}$

end

$\{\{$ FILL$\_$IN$\_$HERE $\}\}->>$

$\{\{$ Z $=$ a $+$ b $+$ c $\}\}$

$\}>.$

Theorem two$\_$loops : forall a b c$,$

outer$\_$triple$\_$valid $($two$\_$loops$\_$dec a b c$).$

Proof.