public class BubbleSort { /*@ requires arr.length > 0; @ ensures (\forall int k, l; 0 <= k && k <= l && l < arr.length; @ arr[k] <= arr[l]); @*/ public void sort(/*@ non_null */ int[] arr) { /*@ loop_invariant i >= 0 && i < arr.length; @ loop_invariant (\forall int k, l; i <= k && k <= l && l < arr.length; arr[k] <= arr[l]); @ loop_invariant (\forall int k, l; @ 0 <= k && k <= i && i < l && l 0; i--) { /*@ loop_invariant i >= 0 && i < arr.length; @ loop_invariant j >= 0 && j <= i; @ loop_invariant (\forall int k, l; i <= k && k <= l && l < arr.length; @ arr[k] <= arr[l]); @ loop_invariant (\forall int k, l; @ 0 <= k && k <= i && i < l && l= arr[j+1]) { int tmp = arr[j]; arr[j] = arr[j+1]; arr[j+1] = tmp; } } } } }