| comment
| - ループ不変条件（英: Loop invariant）とは、計算機科学において、ループの不変条件のこと。ループとは、繰り返し実行されるコードのこと。ループの不変条件とは、ループ実行前にも、反復を実行するたびにも成立する条件のこと。これは、論理アサーションであり、アサーションを使ってコードが書かれることもある。不変条件を知ることは、ループの意味を知るのに重要である。 形式的検証において、特にホーア論理を使った方法では、ループ不変条件は形式的な述語論理で表現され、ループの特徴やループのアルゴリズムを証明するのに使われる。ループ不変条件はループに入る前の段階でも真であり、ループを繰り返すたびにも真である必要がある。これは、ループが終了する際には、ループ不変条件とループ終了条件の両方が真であることが保証される。 ループと再帰の基礎的な類似性により、ループ不変条件を使いループの部分的な正しさを証明するのと、再帰プログラムを構造的帰納法を使い証明するのは、非常に類似している。事実、ループ不変条件は、たいていは、ループと等価な再帰的プログラムで証明しないといけない帰納法の仮説と同じである。
- Niezmiennik pętli – pojęcie używane w projektowaniu, analizie i dowodzeniu poprawności algorytmów. Mówimy, że zdanie P jest niezmiennikiem pętli, jeżeli po każdym jej przebiegu jest ono prawdziwe. W praktyce niezmiennik pętli traktowany jest jako założenie indukcyjne, na podstawie którego wykazuje się prawdziwość kroku indukcyjnego.
- Инвариант цикла — в программировании — логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла. Инварианты используются в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом.
- In der Informatik ist eine Schleifeninvariante eine Sonderform der Invariante, die am Anfang und Ende eines jeden Schleifendurchlaufs und vor und nach der Ausführung der Schleife in einem Algorithmus gültig ist. Sie ist damit unabhängig von der Zahl ihrer derzeitigen Durchläufe. Eine Schleifeninvariante wird zur formalen Verifizierung von Algorithmen benötigt und hilft zudem, die Vorgänge innerhalb einer Schleife besser zu erfassen. Typischerweise beschreiben Schleifeninvarianten Wertebereiche von Variablen und Beziehungen der Variablen untereinander. Da es sich bei der Schleifeninvariante um einen logischen Ausdruck handelt, kann sie entweder wahr oder falsch sein.
- 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.
- Informatikan, begizta inbariante bat baten begizta bat exekutatu aurretik eta ondoren betetzen den propietatea da. Inbariantea da, batzuetan asertzio dei baten kodea erabiliz egiaztatzen dena. Begizta baten inbariantea ezagutzea ezinbestekoa da begiztak duen efektua ondo ulertu ahal izateko.
- In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked within the code by an assertion call. Knowing its invariant(s) is essential in understanding the effect of a loop.
- De manera informal, ciclo invariante es algún predicado o condición que se mantiene en cada iteración de un ciclo. Por ejemplo: int j = 9;for(int i=0; i<10; i++) j--; En este ejemplo se cumple la invariante de ciclo para cada iteración, ya que se mantiene la condición siguiente: i + j == 9 Otra invariante más débil es: i >= 0 && i < 10 //(condición terminal) //o bien j <= 9 && j >= 0 Las invariantes de ciclo sirven para probar que un algoritmo esté correcto.
- 在计算机科学中，循环不变式（loop invariant，或循环不变量、循环不变条件，也有译作循环不变性），是一组在循环体内、每次迭代均保持为真的性质（表达式），通常被用来证明程式或伪码的正确性（有时但较少情况下用以证明算法的正确性）。简单说来，“循环不变式”是指在循环开始和循环中，每一次迭代时为真的性质。这意味着，一个正确的循环体，在循环结束时“循环不变式”和“循环终止条件”必须同时成立。 由于循环和递归的相通，证明带有不变式的循环的部分正确性和证明通过归纳的递归程序的正确性极其相似。 循环不变代码外提（Loop-invariant code motion）是將循环內部不受循環影響的語句或表達式移到循環體之外，和此條目提到的循环不变式無關係。
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
