我需要证明的程序是

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

我需要证明

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

    {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