Exercices de Logique de Hoare

fill_triplet 1. Completez le triplet : { ??? } x = x + 1; { x > 0 } debutant find_invariant 2. Trouvez l'invariant de boucle pour la somme des elements d'un tableau. debutant fill_triplet 3. Completez la postcondition : { x >= 0 && y >= 0 } z = x + y; { ??? } debutant find_invariant 4. Trouvez l'invariant de boucle pour premmin. intermediaire proof_order 5. Ordonnez les regles : affectation, conditionnel, boucle, composition. intermediaire annotated_code 6. Ecrivez les annotations @pre, @post, @invariant, @variant pour la recherche dichotomique. avance fill_triplet 7. Complétez le triplet de Hoare : { ??? } k = 0; j = 0; { j = 0 ∧ k = 0 } debutant find_invariant 8. Trouvez l'invariant de boucle pour cet algorithme qui calcule le maximum d'un tableau. debutant fill_triplet 9. Complétez la précondition : { ??? } x = y; y = temp; { x = Y ∧ y = X } (échange des valeurs initiales X et Y) debutant find_invariant 10. Trouvez l'invariant de boucle pour le tri à bulles (bubble sort). intermediaire annotated_code 11. Écrivez les annotations Hoare (@pre, @post, @invariant, @variant) pour le tri par sélection du minimum. intermediaire fill_triplet 12. Complétez la postcondition de cette boucle while : { n >= 0 } i = 0; while (i < n) { i++; } { ??? } debutant find_invariant 13. Trouvez l'invariant de l'algorithme de fusion de deux tableaux triés. intermediaire annotated_code 14. Écrivez les annotations Hoare complètes pour le calcul de la factorielle (approche itérative). debutant proof_order 15. Ordonnez les règles de Hoare pour prouver {x=X, y=Y} temp=x; x=y; y=temp; {x=Y, y=X} intermediaire fill_triplet 16. Complétez : { ??? } if (x < 0) x = -x; { x = |X| } (où X est la valeur initiale de x) debutant find_invariant 17. Trouvez l'invariant de l'algorithme de Horspool (recherche de motif). avance annotated_code 18. Écrivez les annotations Hoare complètes pour le tri par fusion (merge sort). avance