Witam. Mam taki problem. Mam zadany algorytm sortowania babelkowego z wartownikiem o to pseudokod:

SORT_BUBBLE(n,A)
wart <- n
while wart >= 2
do k <-1
for i <- 1 to wart - 1
do if A[i] > A[i+1]
then A[i] <-> A[i+1]
k <- i
wart <- k

Mam udowodnić poprawność algorytmu
Udało mi się zdefiniować niezmiennik wewnętrznej pętli for oraz udowodnić 3 kroki muszę to samo zrobić dla tej zewnętrznej pętli while no i tutaj się zaciąłem. Może pomożecie zdefiniować chociaż niezmiennik tej zewnętrznej petli ??? Pozdrawiam

Niezmiennik pętli for:
Na początku każdej iteracji pętli for fragment tablicy A[wart ... n] jest posortowany

Niezmiennik pętli while: ???