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.

When parsing an integer from the same string twice, GNATprove doesn't accept that the same integer should be produced twice. How should I rectify this?

Main file:

with String_Problem;

procedure Eq_Test is
begin
   String_Problem.String_Equal("4456");
end Eq_Test;

String_Problem.ads:

package String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   with
       Ghost;
end String_Problem;

String_Problem.adb:

package body String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   is
      X1 : Integer;
      X2 : Integer;
   begin
      X1 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      X2 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      pragma Assert (X1 = X2);
   end String_Equal;
end String_Problem;

GNATProve output:

alr gnatprove
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

string_problem.adb:16:22: medium: assertion might fail
   16 |      pragma Assert (X1 = X2);
      |                     ^~~~~~~
Summary logged in [path]/gnatprove/gnatprove.out