Hoare logic - invariant of loop
There is an issue below:

{s = 0 and j = 0}
while j &lt;= n do begin
  { s + j = (j - 1)j/2 and j &lt;= n + 1}     (*)
    s := s + j;
  { s = (j-1)j/2 and j &lt;= n + 1}           (**)
  { s = j(j+1)/2 and j + 1 &lt;= n + 1} 
    j := j + 1;
  { s = (j-1)j/2 and j &lt;= n + 1 }
end;
{ s = (j-1)j/2 and j &lt;= n + 1 and j &gt; n} 
{s = n*(n+1)/2}


The part marked with ** seems to use a weakening step (sometimes also called a pre- or post- step), moving from { s = (j-1)j/2 and j &lt;= n + 1} to { s = j(j+1)/2 and j + 1 &lt;= n + 1}. However, this is allowed only if the former implies the second, which is not the case! This step looks completely arbitrary.

You can simply avoid it, and backward propagate as usual.

Further, in * you can also assume that the while guard is true, beyond the invariant.

Here's a possible step towards a fix:

{ s = 0 and j = 0 }                           (1)
{ s = (j-1)j/2 and j &lt;= n + 1 }
while j &lt;= n do begin
  { s = (j-1)j/2 and j &lt;= n + 1 and j &lt;= n }  (2)
  { s + j = j(j+1)/2 and j + 1 &lt;= n + 1 } 
    s := s + j;
  { s = j(j+1)/2 and j + 1 &lt;= n + 1 } 
    j := j + 1;
  { s = (j-1)j/2 and j &lt;= n + 1 }
end;
{ s = (j-1)j/2 and j &lt;= n + 1 and j &gt; n }     (3)
{ s = n*(n+1)/2 }


Now you need to prove the implications at points 1,2,3. 3 looks simple, and 2 requires a bit of arithmetic. Instead 1 looks false if n&lt;-1. We need a stronger precondition ensuring that.

Indeed, if you manually run the program starting with n=-10, you do not get s=n(n+1)/2 at the end, so the Hoare triple is invalid, hence -- since the Hoare logic is correct -- we can not hope to prove it valid ;-)