Use the process of postcondition hoisting and proof rules for sequence and assignment to derive the weakest preconditions and the verification conditions for the following specification statements.

{ true }
M := X;
N := Y;
A := 2 * M + N; N := N – 1;
M := A
{ M > N}

I missed a few lectures and I have no idea on how to do this.

I don't have enough material to refer to and this is my first time studying this language. please help me.