Questions tagged [loop-invariants]

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

Filter by
Sorted by
Tagged with
1
vote
0answers
828 views

Correctness of Dijkstra's algorithm

This question is about the correctness proof of Dijkstra's algorithm in the third edition of Introduction to Algorithms by Cormen et al. (pages 660–661). The proof makes a case that considering path $...
2
votes
2answers
2k views

Proof of correctness of algorithms (induction)

I am reading Algorithm's Design Manual by S.Skiena and I have a hard time understanding and proving the correctness of algorithms. I should use proof by induction and when we talk about summations and ...
1
vote
2answers
327 views

Prove correctness of iterative LCM algorithm

I have been trying to prove the following algorithm, without success. Here is the C-Style pseudocode: ...
2
votes
1answer
208 views

How to use the concept of loop invariant to reduce errors in loops?

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Here is an small example ...
3
votes
1answer
956 views

How to find loop invariant from weakest precondition?

Consider this code: Precondition: Postcondition: rv == i <==> ∃i, 0 ≤ i ≤ a.length-1, a[i] == key ...
4
votes
3answers
1k views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
0
votes
1answer
901 views

Proving correctness of a loop that calculates the sum of array

I am trying to mathematically prove that the following program is correct: ...
1
vote
1answer
973 views

Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct? I'm asked to prove (using Hoare Logic) that the following program is valid: ...
1
vote
2answers
2k views

Trouble finding loop invariant for this while loop

I'm having trouble coming up with an invariant for proving partial correctness of this function. ...
7
votes
2answers
793 views

Loop variant for a while loop that occasionally doesn't decrease?

I'm working on practice problems for a test I have, and every example of loop variant decreased with every iteration of the loop. On this one, the values remain the same when a < b. My attempts ...
2
votes
2answers
678 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
2
votes
1answer
462 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 ...
1
vote
1answer
365 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. ...
4
votes
2answers
454 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 ...
2
votes
1answer
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 ...
0
votes
1answer
72 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\}$ ...
1
vote
3answers
185 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 ...
0
votes
0answers
73 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 ...
1
vote
3answers
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 appear ...
2
votes
1answer
277 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 ...
4
votes
1answer
548 views

Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...
7
votes
2answers
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: <...
7
votes
4answers
3k views

Loop invariant for an algorithm

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 ...
10
votes
2answers
1k views

How is the loop invariant obtained in this square root bound finding algorithm?

Originally on math.SE but unanswered there. Consider the following algorithm. ...

1
2