hoare-logic - Repeat until の Hoare ロジック

Question

Hoare Logicを使用するまで、プログラムを繰り返し証明するにはどうすればよいですか?

次のようなルールを見つけました。

{P} S {R}, {R ^ ~B -> P}, {R ^ B -> Q}

{P} の場合、B {Q} まで S を繰り返す

しかし、このルールをどのように使用できるかについての説明はまだ見つかりません

たとえば、この質問では：

{x > 0 ^ y > 0}
     z:=0; u:=x; REPEAT
        z:=z+y;
        u:=u-1;
     UNTIL u=0;
{z = x * y}

ルールを使用してこのプログラムを証明するにはどうすればよいですか?