(b) Prove partial correctness for the following while program. Note that you should clearly identify a loop invariant. a=x;y=1;while}(a>0){y=a;a; The precondition here is x0 and postcondition is y=x