TD6 : Preuve de programmes - Loria
Dans ce TD, nous allons démontrer que les algorithmes étudiés sont corrects en
... La cinqui`eme r`egle, au sujet des boucles, n'est pas tr`es compliquée non
plus, ... chaque boucle while par un invariant et un variant (syntaxe : {inv I var V })
.