Vous devez vous connecter pour exécuter votre code.
Hoare 6 — Tri par insertion avec annotations complètes
Écrivez le code C du tri par insertion avec les annotations Hoare pour la boucle externe ET la boucle interne.
Invariant attendu :
t[0..i-1] est le tri stable de sa valeur initiale
Quantité de contrôle attendue :
n - i
#include <stdio.h>
// @pre: n >= 0
// @post: t est trié en ordre croissant (tri stable)
void tri_insertion(int t[], int n) {
// @invariant: t[0..i-1] est le tri stable de sa valeur initiale
// @variant: n - i
for (int i = 1; i < n; i++) {
int cle = t[i];
int j = i - 1;
// @invariant: t[0..j] trié && t[j+2..i] décalé à droite && cle < t[j+2..i]
// @variant: j + 1
while (j >= 0 && t[j] > cle) {
t[j + 1] = t[j];
j = j - 1;
}
t[j + 1] = cle;
}
}
int main() {
int n, t[1000];
scanf("%d", &n);
for (int i = 0; i < n; i++) scanf("%d", &t[i]);
tri_insertion(t, n);
for (int i = 0; i < n; i++) printf("%d ", t[i]);
printf("\n");
return 0;
}