The following Hoare triple for a program that finds a maximum of 3 numbers is totally correct, in addition to being valid.

{ X ≥ 0 ∧ Y ≥ 0 ∧ Z ≥ 0 }
  x, y, z := X, Y, Z; 
  m := 0;
  do   x > m → m := x
    ⌷  y > m → m := y
    ⌷  z > m → m := z
  od
{ m = max(X, Y, Z) ∧ x = X ∧ y = Y ∧ z = Z ∧ X ≥ 0 ∧ Y ≥ 0 ∧ Z ≥ 0 }

What decreasing variant function could be used to show that the given triple would indeed terminate?

I tried this function, it is decreasing at every iteration and the loop would terminate once it reaches zero:

max(X, Y, Z) − m