/*@
 predicate swap{L1, L2}(int* a, integer i, integer j) =
    \at(a[i], L1) == \at(a[j], L2) && 
    \at(a[j], L1) == \at(a[i], L2) && 
    \forall integer k; 
      k != i && k != j ==> \at(a[k], L1) == \at(a[k], L2);

  inductive permutate{L1, L2}(int* a) {
    case permutate_id{L1}:
      \forall int* a; permutate{L1, L1}(a);
    case permutate_swap{L1, L2}:
      \forall int* a, integer i, integer j;
        swap{L1, L2}(a, i, j) ==> permutate{L1, L2}(a);
    case permutate_trans{L1, L2, L3}:
      \forall int* a;
        permutate{L1, L2}(a) ==> permutate{L2, L3}(a) ==> permutate{L1, L3}(a);
  }
*/

/* Dudu: je ne comprends pas pourquoi tu as changé la signature de ma version 
 * pour remplacer le type de retour `void` par `int *`. Comme pour le tri
 * par sélection qu'on a étudié hier, ce tri est en place, c'est-à-dire que le
 * tableau est modifié directement et la fonction ne retourne aucune valeur. */

/*@
   requires \valid(a + (0 .. sz - 1));
   requires sz > 0;
   ensures \forall integer p; 0 <= p < sz ==> 
    \forall integer  q; 0 <= q < p  ==> a[q] <= a[p]; 
 */  
int* bubble_sort(int* a, int sz) {
  /* Dudu: tu n'as pas besoin de définir ces variables en dehors des boucles
   * afin d'y faire référence dans les invariants de la boucle. Lorsque tu écris
   * ```c
   * for (int i = 0; i < sz; i++) {
   *   ...
   * }
   * ```
   * le scope de la variable `i` est bien limité au bloc de la boucle for mais 
   * tu peux regarder le code C affiché dans frama-c-gui et constater que les 
   * boucles for sont en fait transformées en boucles while et que les 
   * invariants sont insérés après la déclaration de la variable i. Plus précisément:
   * ```c
   * int i = 0;
   * // LES INVARIANTS ICI
   * while (i < sz) {
   *   ...
   *   i++;
   * } */
  int i, j;

  /* Dudu: je ne comprends pourquoi tu as l'invariant `sz`? Remarque que en C
   * les types entiers sont automatiquement convertis en booléen et donc que 
   * la proposition `sz` ici signifie exactement `sz != 0`, ce qui est d'ailleurs 
   * rendu visible par la fonction d'affichage dans l'interface `frama-c-gui`.
   * En particulier cet invariant est impliqué par le second qui stipule déjà 
   * que 0 < sz est toujours vrai. */

  /* Dudu: tu as tout à fait raison, l'invariant I1 n'est pas vrai en entrée 
   * boucle, je pense que tu es sur la bonne voie. */

 /*@
    loop invariant sz; 
    loop invariant 0 <= i < sz;
    loop assigns i, j, a[0..sz-1];
    loop invariant I1: \forall integer p; i <= p < sz ==> 
      \forall integer q; 0 <= q < p  ==> a[q] <= a[p]; 
    loop variant i;
  */
  for (i = sz - 1; i >= 1; i--) {
     /* Dudu: c'est un bon début :D. Ton invariant:
          \forall integer q; 0 <= q < j   ==> a[q] <= a[j];
        stipule que a[j] est un maximum du segment [0..j] du tableau a.
      */

    /* Dudu: comme dans le tri par sélection, l'invariant établit par la boucle
     * extérieure doit être présent dans les invariants de la boucle intérieure,
     * sinon ces informations sont perdues après l'exécution de la boucle. */

     /*@
      loop invariant sz;
      loop invariant 0 <= i < sz;
      loop assigns j, a[0..sz-1];
      loop invariant  \forall integer q; 0 <= q < j   ==> a[q] <= a[j];
      loop invariant 0 <= j <= i;
      loop variant sz - j; 
      */

    for (j = 0; j < i; j++) {
      if (a[j + 1] < a[j]) {
        int tmp = a[j];
        a[j] = a[j + 1];
        a[j + 1] = tmp;
      }
    }
  }
  return a; 
}