| dbpprop:abstract
|
- In computer science, a loop invariant is an invariant used to prove properties of loops. Specifically in Floyd-Hoare logic, the partial correctness of a while loop is governed by the following rule of inference: <math>\frac{\{C\land I\}\;\mathrm{body}\;\{I\}} {\{I\}\;\mathbf{while}\ (C)\ \mathrm{body}\;\{\lnot C\land I\}}</math> This means: A while loop does not have the side effect of falsifying <math>I</math>—if the loop's body does not change an invariant <math>I</math> from true to false given the condition <math>C</math>, then <math>I</math> will still be true after the loop has run as long as it was true before. <math>while(C) ... </math> runs as long as the condition <math>C</math> is true—after the loop has run, if it terminates, <math>C</math> is false. The rule above is a deductive step that has as its premise the Hoare triple <math>\{C\land I\}\;\mathrm{body}\;\{I\}</math>. This triple is actually a relation on machine states. It holds whenever starting from a state in which the boolean expression <math>C\land I</math> is true and successfully executing some program called body, the machine ends up in a state in which <math>I</math> is true. If this relation can be proven, the rule then allows us to conclude that successful execution of the program while (C) body will lead from a state in which <math>I</math> is true to a state in which <math>\lnot C\land I</math> holds. The boolean formula I in this rule is known as the loop invariant. The following example illustrates how this rule works. Consider the program while (x<10) x:= x+1; One can then prove the following Hoare triple: <math>\{x\leq10\}\; \mathbf{while}\ (x<10)\ x := x+1\;\{x=10\}</math> The condition C of the while loop is <math>x<10</math>. A useful loop invariant I is <math>x\leq10</math>. Under these assumptions it is possible to prove the following Hoare triple: <math>\{x<10 \land x\leq10\}\; x := x+1 \;\{x\leq10\}</math> While this triple can be derived formally from the rules of Floyd-Hoare logic governing assignment, it is also intuitively justified: Computation starts in a state where <math>x<10 \land x\leq10</math> is true, which means simply that <math>x<10</math> is true. The computation adds 1 to x, which means that <math>x\leq10</math> is still true (for integer x). Under this premise, the rule for while loops permits the following conclusion: <math>\{x\leq10\}\; \mathbf{while}\ (x<10)\ x := x+1 \;\{\lnot(x<10) \land x\leq10\}</math> However, the post-condition <math>\lnot(x<10)\land x\leq10</math> (x is less than or equal to 10, but it is not less than 10) is logically equivalent to <math>x=10</math>, which is what we wanted to show. The loop invariant plays an important role in the intuitive argument for soundness of the Floyd-Hoare rule for while loops. The loop invariant has to be true before each iteration of the loop body, and also after each iteration of the loop body. Since a while loop is precisely the repeated iteration of the loop body, it follows that if the invariant is true before entering the loop, it must also be true after exiting the loop. Because of the fundamental 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 inductive property one has to prove of a recursive program that is equivalent to a given loop.
- Als Schleifeninvariante werden Eigenschaften einer Schleife in einem Algorithmus bezeichnet, die zu einem bestimmten Punkt bei jedem Schleifendurchlauf gültig sind, unabhängig von der Zahl ihrer derzeitigen Durchläufe. Sie werden zur Verifizierung von Algorithmen benötigt und helfen zudem, die Vorgänge innerhalb einer Schleife besser zu erfassen. Typischerweise beschreiben Schleifeninvarianten Wertebereiche von Variablen und Beziehungen der Variablen untereinander. Zu jeder Schleife lässt sich eine Aussage finden, die vor und nach der Schleife gilt, z. B. eine Tautologie wie „wahr = wahr“. Es ist also stets möglich, eine Invariante anzugeben.
- 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.
|
| rdfs:comment
|
- In computer science, a loop invariant is an invariant used to prove properties of loops.
- Als Schleifeninvariante werden Eigenschaften einer Schleife in einem Algorithmus bezeichnet, die zu einem bestimmten Punkt bei jedem Schleifendurchlauf gültig sind, unabhängig von der Zahl ihrer derzeitigen Durchläufe. Sie werden zur Verifizierung von Algorithmen benötigt und helfen zudem, die Vorgänge innerhalb einer Schleife besser zu erfassen. Typischerweise beschreiben Schleifeninvarianten Wertebereiche von Variablen und Beziehungen der Variablen untereinander.
- 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.
|
![[RDF Data]](/statics/sw-cube.png)
