proof-of-correctness - ループ不変Hoare Logic

Question

ループ不変式を見つけて証明するプログラムがあります。

      {x>=0 && y>=0} // precondition
res:=0;
i:=0;
while (i<y) do
res:=res+x;
i:=i+1;
od
      {res:=x*y} //postcondition

私にとって唯一の論理ループの不変は ですres<=x*y。これは事後条件から簡単ですが、続けるのが最善だとは思いません。多分他の提案はありますか？