logic - 为 Hoare Triple 的部分正确性写一个循环不变量

Question

我是逻辑世界的新手。我正在学习 Hoare Logic 和程序的部分和全部正确性。我尝试了很多解决以下问题但失败了。

Write a loop invariant P to show partial correctness for the Hoare triple

{x = ¬x ∧ y = ¬y ∧ x >= 0} mult {z = ¬x * ¬y}

where mult is the following program that computes the product of x and y and stores it in z:

   mult: 
      z := 0;
      while (y > 0) do
      z := z + x;
      y := y - 1;

我的一位朋友给了我以下答案，但我不知道它是否正确。

Invariant P is (¬x * ¬y = z + ¬x * y) ∧ x = ¬x. Intuitively, z holds the part of the result that is already computed, and (¬x * y) is what remains to compute.

请一步一步教我如何解决这个问题。