/******************************************************************************/ /* Spécification et preuve du Tri-Bulle */ /* Olivier Ly */ /******************************************************************************/ public class TriBulle { /******************************************************/ /*@ requires t != null; */ /*@ requires 0<=i && i 2 */ /*@ modifies t[*] */ /*@ ensures (\forall int i,j; 0<=j && j t[k-1] <= t[i]) for(k=0; k=k && l t[l] <= t[i]) //@ loop_invariant (\forall int i,j; 0<=j && j=k && i t[j] <= t[i]) for(l=t.length-1; l > k; l--) { if (t[l-1] > t[l]) { echange(t,l-1,l); } } } } } /******************************************************************************/ /******************************************************************************/