# Questions tagged [loop-invariants]

Properties that hold before and after every execution of a loop. Used to prove correctness of algorithms.

64 questions
Filter by
Sorted by
Tagged with
631 views

### Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
438 views

### Finding a good loop invariant

I want to prove that the following program is correct. The code takes an array i of length N and a number ...
316 views

### Loop invariant: decreasing a variable and swapping it

As an example exercise, we were asked to find the loop invariant for this bit of code. ...
438 views

### Loop-invariant code motion with unsafe operations

There are well-known algorithms LICM, and they work well. Unfortunately, there are certain cases when these optimizations can cause runtime failures with code that was initially correct. Consider the ...
3k views

### Proof of Program Correctness - Loop Invariants

I've been reading a book on using loop invariants and induction to prove program correctness. Then I came across the following program which got me thinking... Specification for ...
67 views

### Does this loop invariant guarantee that the variable never changes?

Suppose you have some loop and and integer k: int k = 5; for (int i = 0 ; i < N; i++) { //(*) //do something } The loop invariant at (*) is: $\{ K=k\}$ ...
176 views

### Loop Invariants as Tautologies

Would it be correct to characterize loop invariants as a type of tautology? I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop ...
67 views

### loop invariant proof [duplicate]

Possible Duplicate: Proof of linear search? I'm reading the MIT Press, Introduction to Algorithms textbook 3rd edition, and I am a bit confused by an exercise. 2.1-3 Consider the searching ...
2k views

### Proof of linear search?

Consider the searching problem: Input: A sequence of $n$ numbers $A=(a_1, a_2, \ldots , a_n)$ and a value $v$. Output: An index $i$ such that $v = a_i$ or the special value NIL if $v$ does not ...
259 views

### Invariant Proof of For Loops?

From CLRS (third edition, page 19), there is a footnote: When the loop is a for loop, the moment at which we check the loop invariant just prior to the first iteration is immediately after the ...
515 views

### Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...
2k views

### Invariant For Nested Loop in Matrix Multiplication Program

I'm making a graduate thesis about proving correctness of program for multiplying 2 matrices using Hoare logic. For doing this, I need to generate the invariant for nested loop for this program: <...
I have developed the following pseudocode for the sum of pairs problem: Given an array $A$ of integers and an integer $b$, return YES if there are positions $i,j$ in $A$ with $A[i] + A[j] = b$, NO ...