Need help with Bubblesort

[pecel]

procedure bubblesort;
var i, t, integer;
begin
repeat until t = a[1]
t:=a[1];
for j:=2 to n do
if a[j-1] > a[j] then begin
t:= a[j-1];
a[j-1]:=a[j];
a[j]:=t;
end
end rep
end

Partition the design into sub functions, and define a set of conditions that would enable you to prove that this algorithm is correct.

Thanks.