Hoare logic - invariant of loop [closed]

I am trying to prove partial corectness of following program:

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

And I am trying to find invariant. It seems to me that good candidate is s = (j-1)j/2 and j <= n + 1.
Am I ok ?

closed as unclear what you're asking by David Richerby, Evil, Rick Decker, Juho, Tom van der ZandenJul 5 '16 at 21:33

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• Looks as it should work to me. Have you tried writing the proof? – chi Jun 28 '16 at 17:14
• I tried, I show you it in a moment, look at it please. – user54001 Jun 28 '16 at 17:49

There is an issue below:

{s = 0 and j = 0}
while j <= n do begin
{ s + j = (j - 1)j/2 and j <= n + 1}     (*)
s := s + j;
{ s = (j-1)j/2 and j <= n + 1}           (**)
{ s = j(j+1)/2 and j + 1 <= n + 1}
j := j + 1;
{ s = (j-1)j/2 and j <= n + 1 }
end;
{ s = (j-1)j/2 and j <= n + 1 and j > 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 <= n + 1} to { s = j(j+1)/2 and j + 1 <= 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 <= n + 1 }
while j <= n do begin
{ s = (j-1)j/2 and j <= n + 1 and j <= n }  (2)
{ s + j = j(j+1)/2 and j + 1 <= n + 1 }
s := s + j;
{ s = j(j+1)/2 and j + 1 <= n + 1 }
j := j + 1;
{ s = (j-1)j/2 and j <= n + 1 }
end;
{ s = (j-1)j/2 and j <= n + 1 and j > 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<-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 ;-)

• It looks like we should add condition  n >= 0 at begin and propagate it. However, without this condition our program is looping for n<1 - but is something wrong ? Our program is still partially correct. – user54001 Jun 30 '16 at 8:15
• Ok, now I think that we should prove implication: (beyond (2) and (3)) { s = 0 and j = 0 } => { s = (j-1)j/2 and j <= n + 1 }. However, for n<0 we can't prove it. Now, Am I ok ? – user54001 Jun 30 '16 at 8:17
• @HaskellFun It is true that partial correctness does not imply that the program terminates, but the program above does terminate: whatever n is, j will eventually be larger than it. – chi Jun 30 '16 at 8:49
• Ok, so me second comment is ok ? – user54001 Jun 30 '16 at 8:52
• look again here also, please: cs.stackexchange.com/questions/60167/… – user54001 Jun 30 '16 at 8:52