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

learn more… | top users | synonyms

-1
votes
0answers
17 views

while loop program corectness - invariant and hoare logic

Could someone verify my proof in hoare logic ? It is about invariant for loop while, look: ...
1
vote
1answer
82 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 ...
2
votes
1answer
67 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
207 views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
-1
votes
1answer
54 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
98 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: ...
0
votes
2answers
73 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
140 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
124 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
2
votes
1answer
224 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
96 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. ...
3
votes
2answers
163 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
2k 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
52 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
115 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
45 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
2answers
1k 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 ...
2
votes
1answer
204 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
265 views

Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...
7
votes
2answers
856 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
984 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
664 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. ...