algorithm - if 语句完全正确性的证明

Question

我需要证明的程序是

if(x>y){
   z=x;
}else{
   z=y;
}

而且我需要证明（这里的P应该是上面的程序）是有效的，我能做的就是证明它的部分正确性，但是如何证明它的全部正确性呢？

这是我对部分正确性的证明：

    {T}
    {(x>y -> x=max(x,y) ) ∧ (\neg(x>y) -> y=max(x,y) ) }  
    if (x>y)
        {T∧x>y}   If-statement
        {x=max(x,y)}   Implied
   z=x
        {z=max(x,y)}  Assignment
   else
        {T∧¬(x>y)}  If-statement
        {y=max(x,y)}  Implied
    z=y
        {z=max(x,y)}  Assignment
    fi  
        {z=max(x,y)}  If-statement