What is a Proof of Correctness:
Algorithms are identified with pre-conditions and post-conditions. The pre-conditions are assumptions you make about the algorithm's inputs. Post-conditions describe what we want the algorithm to have accomplished once it terminates.
For an algorithm to be considered "partially correct", whenever the pre-conditions hold, the post-conditions must follow. For it to be considered "totally correct", it must be partially correct and halt, i.e. take a finite number of steps.
Pre and post-conditions are something one specifies about an algorithm, not something one proves about it. A typical precondition for a sorting algorithm might be "A[1...n] is an array of integers". A typical postcondition might be "A[1...n] is a sorted array of integers with the same values it had before the algorithm was executed".
That's a lot of formalism to get out of the way before we even talk about the problem, but it's important to be rigorous.
Showing Bubblesort is correct
To show Bubblesort is correct, we should show that the post-conditions follow assuming the pre-conditions hold. Total correctness will follow since Bubblesort trivially halts.
Loop Invariants
This is something you see everywhere in proofs of correctness that have loops. Instead of talking about the whole algorithm "at once", it's useful to come up with something that will be true for each iteration of the loop. This often lends itself to an inductive argument. The loop invariant you want to come up with is something that will help you conclude what you want to conclude at the end of the day - that A[1...n] is sorted once we terminate.
Here's what I came up with to that end. For any iteration $i$ of the outer loop: For any $a \in \{1,...,n\}$:
If there is a $b \in \{1,...,n\}$ such that $a>b$ but $A[a]<A[b]$ at the start of the iteration, then at some point in the inner loop, $A[a]$ and $A[a-1]$ will swap. Similarly, if there is a $b>a$ such that $A[a]>A[b]$, then $A[b]$ and $A[b+1]$ will have swap at some point in the inner loop.
Else, $A[a]$ won't change.
To prove this, it would be helpful to first show that whenever an $a$ satisfies the conditions in the "If" part, $a \leq i$ is true. This lemma could use an inductive argument. By the way this is one (possible clunky) way of coming up with the invariants, you might have a more concise way of phrasing what you need. I haven't written the full proof so I might have inefficiencies up there.
Wrapping Up
Once you show the loop invariants above are true, we can use them to conclude that $A[1..n]$ comes out the other end a sorted list of integers. Let $A[1..n]$ refer to the original list, and $A'[1...n]$ refer to the modified list. Let $a \in \{1,...,n\}$ be arbitrary, and let $c \in \{1,...,n\}$ be a correct sorted index of $A[a]$ in $A[1..n]$, i.e. $c$ is the index $A[a]$ should be at in a sorted version of $A$. We want to show that $A'[c]=A[a]$.
If $a$ was already in it's correct position in $A[1..n]$ (i.e. $a=c$) then we're done, because this means for any $b < a$, $A[b]<A[a]$, thus the swap condition in the inner loop will never be satisfied, meaning $A'[a]=A[a]$. Otherwise, either there exists some $b<a$ such that $A[b] > A[a]$, or some $b>a$ such that $A[b]<A[a]$. In either case, the loop invariants tell us that $A[a]$ will move at least one step in the correct direction after each outer-loop iteration. The maximum distance between $a$ and $c$ is $n-1$, and since the "Else" of the loop invariant essentially tells us that $A[a]$ will stop moving when $a=c$, we can say that $A[a]$ will get to index $c$ and stop, so $A'[c]=A[a]$ as required.
That's the gist of it, I left out the proofs of the invariants, and there might be other gaps in my response. Hopefully you can fill those in. Sorry for the long answer.
