From f2f97634bb196298dcf16339ab79d1a4487feae9 Mon Sep 17 00:00:00 2001 From: Spectre Date: Wed, 27 Nov 2024 08:22:54 +0100 Subject: [PATCH] preuve de terminaison --- preuve.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 preuve.md diff --git a/preuve.md b/preuve.md new file mode 100644 index 0000000..daa3459 --- /dev/null +++ b/preuve.md @@ -0,0 +1,15 @@ +```plaintext +maxi(liste) +precondition: |liste| > 0 + Resultat <- liste[0] + index <- 1 + while index < |liste| + if liste[index] > Resultat + resultat <- liste[index] + index <- index + 1 + Resultat +``` +# Preuve de terminaison + La terminaison est assuré par la présence d'un variant de boucle (séquence d'entier naturel). *ici* ```plaintext +|liste| - index +```est un variant de boucles