Consider this program fragment (assume we are using all integers):

{ PRE: x0 = x and y0 = y } if (x > y) then y := x else x := y { POST: x = y = max(x0,y0) }Prove that the program fragment is correct with respect to the given PRE and POST specifications...