Finding the weakest precondition and invariant of while loop

I am trying to find the weakest precondition and invariant of this while loop. I have read and am trying to understand the concept of calculating preconditions based on postconditions. I was wondering if someone could explain it to me.

while i < j do
i = i + 1;
j = j - 1;
end

{i = j or i = j + 1}

• Loop invariant here is i<j., As you can clearly see. – Mr. Sigma. Feb 16 '17 at 7:21
• @Seeker I doubt that $i<J$ is strong enough as a loop invariant to reach the desired post-condition. – Martin Berger Feb 16 '17 at 10:39
• @Martin Don't you think Compliment of what inside {} is loop invariant here? Right? – Mr. Sigma. Feb 16 '17 at 10:46
• @Seeker I'm not sure what you mean. – Martin Berger Feb 16 '17 at 11:55
• @Johnny Hmmm, try this with i = 2 and j = 0 ... – Martin Berger Mar 2 '17 at 9:59