Some hints for the Problems to Study By (CMSC 631)

3)  Hoare Logic

a)  {M>=0}  X:=0; N:=1; while N<=M do begin X:=X+N; N:=N+1; end: 
                                   {X = M*(M+1) DIV 2 }

     INV:  { X = (N-1)*N DIV 2  &  N<=M+1 }

b)  {X=x ^ Y=y}
    S:=0;
    while ~(X=0) do
       begin 
         while ~(odd X) do
           begin Y:=2*Y; X:=X DIV 2 end;
         S:=S+Y;
         X:=X-1;
       end;
     {S = x*y }


    INV:  {S + (X*Y) = x*y}