I am new to the world of logic. I am learning Hoare Logic and Partial & Total correctness of programs. I tried alot to solve the below question but failed.
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;
One of my friend gave me the following answer but I don't know if it correct or not.
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.
Please teach me step by step of how to solve this question.