add some exercice

This commit is contained in:
2024-11-27 09:51:07 +01:00
parent 2b5800c112
commit 8f80a875bf
4 changed files with 157 additions and 0 deletions

23
algo2.md Normal file
View File

@@ -0,0 +1,23 @@
```Plaintext
somme(liste)
somme = 0
idx = 0
while idx < |liste|
somme = somme + liste[idx]
idx = idx + 1
```
# Myself
## Preuve de terminaison
La *Terminaison* est assurée par un variant de boucle (ici idx < |liste| est un variant de boucle)
```plaintext
|liste| - idx
```
est ici l'ivariant de boucle
## Preuve de correction partielle
La correction partielle est assurée par *l'invariant de boucle* ici Somme contient toutes les valeurs de la liste ajouter les unes aux autres ? par
```Plaintext
somme = somme + liste[idx]
```
## Conclusion L'algo se termine et, à la sortie, idx = |liste| et somme contient tous les elements de la liste additionés entre eux