hoare-logic - 重复直到的霍尔逻辑

Question

在使用 Hoare Logic 之前，我们如何重复证明一个程序？

我发现了这样的规则：

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

对于 {P} 重复 S 直到 B {Q}

但我仍然找不到任何解释如何使用此规则

例如在这个问题中：

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

我如何使用该规则来证明这个程序？