| dbo:abstract
|
- 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. Zu jeder Schleife lässt sich eine Invariante finden, die vor der Schleife und nach jeder Prüfung der Schleifenbedingung gilt, z. B. eine Tautologie wie „wahr = wahr“. Es lässt sich also immer eine Invariante bestimmen, diese ist aber nicht immer dafür geeignet, einen formalen Korrektheitsbeweis durchzuführen. (de)
- 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. (eu)
- 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. (es)
- 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. In formal program verification, particularly the Floyd-Hoare approach, loop invariants are expressed by formal predicate logic and used to prove properties of loops and by extension algorithms that employ loops (usually correctness properties).The loop invariants will be true on entry into a loop and following each iteration, so that on exit from the loop both the loop invariants and the loop termination condition can be guaranteed. From a programming methodology viewpoint, the loop invariant can be viewed as a more abstract specification of the loop, which characterizes the deeper purpose of the loop beyond the details of this implementation. A survey article covers fundamental algorithms from many areas of computer science (searching, sorting, optimization, arithmetic etc.), characterizing each of them from the viewpoint of its invariant. Because of the similarity of loops and recursive programs, proving partial correctness of loops with invariants is very similar to proving correctness of recursive programs via induction. In fact, the loop invariant is often the same as the inductive hypothesis to be proved for a recursive program equivalent to a given loop. (en)
- 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)
- ループ不変条件（英: Loop invariant）とは、計算機科学において、ループの不変条件のこと。ループとは、繰り返し実行されるコードのこと。ループの不変条件とは、ループ実行前にも、反復を実行するたびにも成立する条件のこと。これは、論理アサーションであり、アサーションを使ってコードが書かれることもある。不変条件を知ることは、ループの意味を知るのに重要である。 形式的検証において、特にホーア論理を使った方法では、ループ不変条件は形式的な述語論理で表現され、ループの特徴やループのアルゴリズムを証明するのに使われる。ループ不変条件はループに入る前の段階でも真であり、ループを繰り返すたびにも真である必要がある。これは、ループが終了する際には、ループ不変条件とループ終了条件の両方が真であることが保証される。 ループと再帰の基礎的な類似性により、ループ不変条件を使いループの部分的な正しさを証明するのと、再帰プログラムを構造的帰納法を使い証明するのは、非常に類似している。事実、ループ不変条件は、たいていは、ループと等価な再帰的プログラムで証明しないといけない帰納法の仮説と同じである。 (ja)
- 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. (pl)
- Инвариант цикла — в программировании — логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла. Инварианты используются в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом. (ru)
- 在计算机科学中，循环不变式（loop invariant，或循环不变量、循环不变条件，也有译作循环不变性），是一组在循环体内、每次迭代均保持为真的性质（表达式），通常被用来证明程式或伪码的正确性（有时但较少情况下用以证明算法的正确性）。简单说来，“循环不变式”是指在循环开始和循环中，每一次迭代时为真的性质。这意味着，一个正确的循环体，在循环结束时“循环不变式”和“循环终止条件”必须同时成立。 由于循环和递归的相通，证明带有不变式的循环的部分正确性和证明通过归纳的递归程序的正确性极其相似。 循环不变代码外提（Loop-invariant code motion）是將循环內部不受循環影響的語句或表達式移到循環體之外，和此條目提到的循环不变式無關係。 (zh)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 17507 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:date
| |
| dbp:reason
|
- I guess, once the notion of 'loop-invariant code' is defined in a sufficiently formal way, it can be proven that loop-invariant code *always* induces a corresponding loop invariant property. (en)
|
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- 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. (eu)
- 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. (es)
- ループ不変条件（英: Loop invariant）とは、計算機科学において、ループの不変条件のこと。ループとは、繰り返し実行されるコードのこと。ループの不変条件とは、ループ実行前にも、反復を実行するたびにも成立する条件のこと。これは、論理アサーションであり、アサーションを使ってコードが書かれることもある。不変条件を知ることは、ループの意味を知るのに重要である。 形式的検証において、特にホーア論理を使った方法では、ループ不変条件は形式的な述語論理で表現され、ループの特徴やループのアルゴリズムを証明するのに使われる。ループ不変条件はループに入る前の段階でも真であり、ループを繰り返すたびにも真である必要がある。これは、ループが終了する際には、ループ不変条件とループ終了条件の両方が真であることが保証される。 ループと再帰の基礎的な類似性により、ループ不変条件を使いループの部分的な正しさを証明するのと、再帰プログラムを構造的帰納法を使い証明するのは、非常に類似している。事実、ループ不変条件は、たいていは、ループと等価な再帰的プログラムで証明しないといけない帰納法の仮説と同じである。 (ja)
- 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. (pl)
- Инвариант цикла — в программировании — логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла. Инварианты используются в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом. (ru)
- 在计算机科学中，循环不变式（loop invariant，或循环不变量、循环不变条件，也有译作循环不变性），是一组在循环体内、每次迭代均保持为真的性质（表达式），通常被用来证明程式或伪码的正确性（有时但较少情况下用以证明算法的正确性）。简单说来，“循环不变式”是指在循环开始和循环中，每一次迭代时为真的性质。这意味着，一个正确的循环体，在循环结束时“循环不变式”和“循环终止条件”必须同时成立。 由于循环和递归的相通，证明带有不变式的循环的部分正确性和证明通过归纳的递归程序的正确性极其相似。 循环不变代码外提（Loop-invariant code motion）是將循环內部不受循環影響的語句或表達式移到循環體之外，和此條目提到的循环不变式無關係。 (zh)
- 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. (de)
- 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. (en)
- 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
|
- Schleifeninvariante (de)
- Ciclo invariante (es)
- Begizta inbariante (eu)
- Invariant de boucle (fr)
- Loop invariant (en)
- ループ不変条件 (ja)
- Niezmiennik pętli (pl)
- Инвариант цикла (ru)
- 循环不变量 (zh)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
