En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme. En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes.

Property Value
dbo:abstract
  • En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme. En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes. Un invariant de boucle doit être vrai avant de commencer la boucle et il est garanti qu'il restera vrai après chaque itération de la boucle. En particulier, l'invariant sera toujours vrai à la fin de la boucle.Les boucles et la récursivité étant fondamentalement similaires, il y a peu de différence entre démontrer un invariant de boucles et prouver qu'un programme est correct en utilisant un raisonnement par récurrence. En pratique, l'invariant de boucle est souvent la propriété induction — l'hypothèse d'induction — qui sert à montrer qu'un programme récursif est équivalent à une boucle. (fr)
  • En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme. En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes. Un invariant de boucle doit être vrai avant de commencer la boucle et il est garanti qu'il restera vrai après chaque itération de la boucle. En particulier, l'invariant sera toujours vrai à la fin de la boucle.Les boucles et la récursivité étant fondamentalement similaires, il y a peu de différence entre démontrer un invariant de boucles et prouver qu'un programme est correct en utilisant un raisonnement par récurrence. En pratique, l'invariant de boucle est souvent la propriété induction — l'hypothèse d'induction — qui sert à montrer qu'un programme récursif est équivalent à une boucle. (fr)
dbo:isPartOf
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 9017784 (xsd:integer)
dbo:wikiPageLength
  • 6167 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 185416453 (xsd:integer)
dbo:wikiPageWikiLink
prop-fr:fr
  • Variant de boucle (fr)
  • Variant de boucle (fr)
prop-fr:trad
  • Loop variant (fr)
  • Loop variant (fr)
prop-fr:wikiPageUsesTemplate
dct:subject
rdfs:comment
  • En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme. En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes. (fr)
  • En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme. En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes. (fr)
rdfs:label
  • Invariant de boucle (fr)
  • Niezmiennik pętli (pl)
  • Schleifeninvariante (de)
  • Инвариант цикла (ru)
  • ループ不変条件 (ja)
  • Invariant de boucle (fr)
  • Niezmiennik pętli (pl)
  • Schleifeninvariante (de)
  • Инвариант цикла (ru)
  • ループ不変条件 (ja)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageWikiLink of
is oa:hasTarget of
is foaf:primaryTopic of