Inscription / Connexion Nouveau Sujet
Invariant de boucle
Bonjour,
Pour commencer voici le problème:
Il s'agit, dans cet algorithme, de convertir une date donnée sous forme du
nombre de jours depuis le 1er janvier 2005, en une date qui donne l'année et le numéro de jour de l'année.
On est doté d'une fonction EstAnneeBissextile(annee) qui détermine si annee est bissextile ou
non (pour rappel, une année est bissextile lorsqu'elle est divisible par 4 mais pas par 100, sauf si elle divisible
par 400). Une année bissextile a un 29 février, et donc 366 jours au lieu de 365 jours normalement.
# ‘jour' est initialement la date en jours écoulés depuis le 01/01/2005 , annee = 2005
**************************************************************************
while jour > 365:
if EstAnneeBissextile(annee):
if jour > 366:
jour = jour - 366
annee = annee + 1
else:
jour = jour - 365
annee = annee + 1
print "Aujourd'hui nous sommes le", jour, "ieme jour de l'année", annee
***************************************************************************
Si le code est incorrect, corrigez-le. Faites une preuve de terminaison, trouvez l'invariant de boucle, puis
donnez enfin une preuve de correction (ou expliquez au moins comment vous prouveriez votre invariant de
boucle).
Indications : vous pourrez considérer le déroulement du programme pour la valeur initiale jour = 1461 ;
pour l'invariant de boucle, vous pourrez vous servir de la fonction mathématique nbBissextile(x) qui calcule
le nombre d'années bissextiles comprises entre 2005 et x, l'année x non incluse — ainsi, par exemple,
nbBissextile(2012) = 1 et nbBissextile(2013) = 2.
Je commence l'algorithmique, et avec les exemples je pensais bien comprendre mais quand il s'agit de le faire, c'est une autre histoire...
Avec la première piste, on s'aperçoit que le code est faux, en effet si jour=366 est que l'année est bissextile, la boucle est infinie, donc pour corriger cela j'ai modifié la première ligne:
while (jour>365 and (not EstAnneeBissextile(annee)) or (jour>366 and EstAnneeBissextile(annee))...
Ca me semble correct mais il y a peut être plus simple.
-Terminaison: Preuve informelle:
Avec ces nouvelles conditions, la variable jour décroit à chaque passage dans la boucle, donc la boucle s'arrête.
L'invariant de boucle, c'est la mon gros problème, je sèche...
Et je ne suis pas sur d'avoir compris la preuve de correction, donc dites moi si je me trompe, il me semble qu'elle est composée de la preuve de terminaison et de la preuve de l'invariant de boucle.
Petite question subsidiaire, l'invariant est il unique?
Merci!
Bon j'ai peut être une réponse:
soit x et y les valeurs initiales respectivement de jour et annee, on a
x=(annee-y)*365+jour+estBissextile(annee)
Et je travaille à la preuve de correction...
Preuve de correction
Soit jour' et annee' les nouvelles valeurs en sortie de jour et annee,
jour'= jour - 365 (-1 si annee est bissextile)
annee'=annee+1
En remplaçant les nouvelles valeurs dans l'invariant:
x=(annee+1-y)*365 + jour - 365 (-1 si annee est bissextile) +nbbissextile(annee+1) = (annee-y)*365 + jour + nbbissextile(annee)
car si annee est bissextile on a
nbBissextile(annee) + 1 = nbBissextile(annee+1) et on retranche 1 au total si l'année est bissextile...
Je suis un peu en terre inconnue donc si ça parait correcte ou incorrecte à quelqu'un...
Merci
Bonjour
Le code n'est toujours pas correct. Si je lance ton algorithme avec jour=0, il me dira que je suis au 0ème jour de l'année 2005, alors que s'il s'est écoulé 0 jours depuis le 1er janvier 2005, je suis toujours le 1er janvier 2005, et donc je suis au 1er jour de l'année.
Pour l'invariant de boucle, il est en général plus simple et intuitif (et pas moins correct) de l'exprimer en français. L'algorithmique est une branche des mathématiques qui se prête mal à un symbolisme excessif.
"Au début de chaque itération de la boucle, la variable jour représente la date voulue exprimée en nombre de jours écoulés depuis le 1er janvier de l'année représentée par la variable annee."
C'est quand même plus clair, non ?
Bonjour,
Je propose (juste une idée avec une syntaxe que je ne connais pas) :
jour = jour + 1
while jour > 366:
jour = jour - 365
annee = annee + 1
if EstAnneeBissextile(annee):
jour = jour - 1
end if (En Basic, c'est la fin de l'instruction if)
wend (En Basic, c'est la fin de boucle while)
if jour=366 and (not EstAnneeBissextile(annee)):
jour = 1
annee = annee + 1
print "Aujourd'hui nous sommes le", jour, "ieme jour de l'année", annee
En effet j'avais loupé cette erreur, d'où le jour=jour+1 de Chatof en début d'algorithme, sinon on est décalé d'un jour...
Pour l'invariant en français, oui, en effet c'est plus clair, mais ça me parait moins pratique pour en tirer une preuve de correction.
@Chatof= Ca me parait bien (et merci pour le jour=jour+1 que j'avais zappé) mais ça me paraît compliquer un peu l'algo de départ.
Merci Bachstelze
(et merci pour le jour=jour+1 que j'avais zappé)
Hélas, je n'avais rien vu!
Il faut remercier Bachstelze.
Dans ma réponse, la preuve de terminaison est facile.
Pour l'invariant de boucle, je m'inspire de
X= jour + annee*365 + nbBissextile(annee)
Je pense qu'il faut alléger la boucle pour gagner de la vitesse (ou temps machine).
Juste 2 tests et un appel de procédure par tour de boucle.
Annuler
connectez vous