Loop invariant for an algorithm
First simplification: this algorithm, by inspection, cannot say YES when it shouldn't, since saying YES is immediately after a test verifying that the sum at the current positions is $b$.  

Second simplification: It always terminates, since $i$ and $j$ move in a monotone way up and down respectively, and one always moves.  Thus, eventually they become equal and the loop ends.

So let's assume that that answer is YES, and $x$ and $y$ are the indices we are interested in, after sorting, with $x$ as small as possible and then $y$ as large as possible (we may have several possible pairs with the right sum).  Here is the invariant:


At the start of the loop, $i\le x$ and $j\ge y$.


If $i=x$ and $j=y$, then the algorithm will stop and say YES.  The loop invariant is trivial at the start, and also trivial when $i&lt;x$ and $j&gt;y$.  But if $i=x$, and $j&gt;y$, then, since the array is sorted $A[i]+A[j]&gt;b$, because of how $y$ was selected.  So $j$ decreases in all future iterations until it reaches $y$.  The other case, where $j$ gets to $y$ first is symmetric.

As noted above, the algorithm always terminates, which implies the algorithm will actually say YES, so we are done.

Edit: Since this question is about proof writing, here is another option, which I think is more confusing and more gritty.  I do not know if Tony Hoare would approve or not.

Here is the invariant:  A the top of the loop,


If $s&lt;i$, then, for any $x\in [n]$, $A[s] + A[x] \neq b$
If $t&gt;j$, then, for any $x\in [n]$, $A[x] + A[t]\neq b$


Again, this holds vacuously at the beginning.  Now we check some cases:


If $i = j$, then in any pair of indices $x$ and $y$ at least one of $x$ or $y$ is smaller than $i$ or bigger than $j$.  This rules out the input being a YES.  The loop ends and says NO, so we are in good shape.
Assume the loop did not end. If $A[i] + A[j] = b$, the answer is YES, and the algorithm works.
Assume $A[i] + A[j] \neq b$. 
Subcase: If there is a $j&#39;$, by hypothesis $j&#39;&lt;j$, such that $A[i] + A[j&#39;] = b$, then $A[j&#39;] &lt; A[j]$ because the array was sorted, so $A[i] + A[j] &gt; b$, which causes $j$ to decrease.  This shows that the invariant is maintained for $i$.  To see it for $j$, just note that if there is an $x$ such that $A[x] + A[j] = b$, then $x &lt; i$, which is ruled out by the inductive hypothesis.
Subcase: If there is a $i&#39;$, by hypothesis $i&#39;&gt;i$, such that $A[i&#39;] + A[j] = b$, then $A[i&#39;] &gt; A[i]$ because the array was sorted, so $A[i] + A[j] &lt; b$, which causes $i$ to increase.  This shows that the invariant is maintained for $j$.  To see it for $i$, just note that if there is an $x$ such that $A[i] + A[x] = b$, then $x &gt; j$, which is ruled out by the inductive hypothesis.
Subcase: If neither of the other two cases holds, then the invariant is maintained trivially.


Finally, we note that the gap between $i$ and $j$ always gets smaller, so they must eventually become equal, and the algorithm will stop.

Remarks: This is the exact same argument, but more difficult to follow.  You too can write proofs like this using some expert techniques:


Don't say what the algorithm does.  Here, if the input is a YES, the algorithm ALWAYS gives you certifying indices that are as close to the ends as possible.  The 2nd proof cleverly hides this in a case analysis.
Don't give names to things.  Having hidden what the algorithm does, also don't name the stopping point.
Don't factor out easy cases.  This algorithm clearly works for NO instances.  By not noting that up front, we get a more complicated invariant.