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