@pre  true
@post true
int[] BubbleSort(int[] a_0) {
	int[] a := a_0;
	for
		@ i + 1 >= 0
		# (i + 1, i + 1)
		(int i := |a| - 1; i > 0; i := i - 1)
	{
		for
			@ i + 1 >= 1 && i - j >= 0
			# (i + 1, i - j)
			(int j := 0; j < i; j := j + 1)
		{
			if (a[j] > a[j + 1]) {
				int t := a[j];
				a[j] := a[j + 1];
				a[j + 1] := t;
			}
		}
	}
	return a;
}