Vous devez vous connecter pour exécuter votre code.
Hoare 3 — Maximum avec annotations
Écrivez le code C d'une fonction qui trouve le maximum d'un tableau non vide, avec annotations Hoare.
Invariant attendu :
1 <= k <= n && max = maximum de t[0..k-1]
Quantité de contrôle attendue :
n - k
#include <stdio.h>
// @pre: n > 0
// @post: retourne le maximum de t[0..n-1]
// @invariant: 1 <= k <= n && max = maximum de t[0..k-1]
// @variant: n - k
int maximum(int t[], int n) {
int max = t[0], k = 1;
while (k < n) {
if (t[k] > max) max = t[k];
k = k + 1;
}
return max;
}
int main() {
int n, arr[1000];
scanf("%d", &n);
for (int i = 0; i < n; i++) scanf("%d", &arr[i]);
printf("%d\n", maximum(arr, n));
return 0;
}