Vous devez vous connecter pour exécuter votre code.
Hoare 1 — Factorielle avec annotations
Écrivez le code C de la fonction factorielle itérative en incluant obligatoirement les annotations Hoare en commentaires : @pre, @post, @invariant, @variant.
La factorielle de n (notée n!) est le produit 1×2×...×n. Par convention, 0! = 1.
Invariant attendu :
f = (k-1)! && 1 <= k <= n+1
Quantité de contrôle attendue :
n - k + 1
#include <stdio.h>
// @pre: n >= 0
// @post: retourne n!
// @invariant: f = (k-1)! && 1 <= k <= n+1
// @variant: n - k + 1
int factorielle(int n) {
int f = 1, k = 1;
while (k <= n) {
f = f * k;
k = k + 1;
}
return f;
}
int main() {
int n;
scanf("%d", &n);
printf("%d\n", factorielle(n));
return 0;
}