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.

この問題の解き方を順を追って教えてください。