Questions tagged [loop-invariants]

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

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

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
4
votes
2answers
432 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 ...
4
votes
1answer
88 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
4
votes
1answer
497 views

Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...
3
votes
1answer
492 views

Loop invariant for a division algorithm

I'm having problems trying to understand the concept of loop invariants. I have the following code, where M and N are predefined constants. ...
3
votes
1answer
800 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 ...
3
votes
2answers
162 views

Invariant on “Find K Closest Elements” problem

I run across this problem: Given a sorted array, two integers k and x, find the k closest ...
3
votes
0answers
236 views

Expression of the weakest precondition of a while loop

I am interested in computing weakest preconditions (WP) of loops. If I refer to Wikipedia "Predicate Transformer semantics", the WP for e.g. total correction of a loop annotated with an invariant I ...
2
votes
1answer
250 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 ...
2
votes
1answer
113 views

Find the loop invariant of the given while loop

I don't know how to find a loop invariant. I'm not sure where to start. Can anyone find the loop invariant of the given program and explain your method please. ...
2
votes
1answer
430 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 ...
2
votes
2answers
186 views

Iterative Fibonacci algorithm correctness proof, finding loop invariants

The algorithm take in an integer $n$ and outputs the $n$th number in the Fibonacci sequence ($F_n$). The sequence starts with $F_0$. I am trying to prove the correctness assuming valid input: ...
2
votes
1answer
772 views

Proving the loop invariant for a simple program in Hoare logic

I was studying loop invariant and came across Tomas Petricek's example. Here's the equivalent(I believe) program after I revised it a bit for proof in Hoare logic: ...
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 ...
2
votes
1answer
261 views

Finding a loop invariant

the following pseudo code returns the nth Fibonacci number: ...
2
votes
2answers
1k 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 ...
2
votes
2answers
621 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
2
votes
1answer
50 views

How to prove a bound function for a sequence of numbers?

Let $G_n$ be defined by $$G_n = \begin{cases} 1 & n=0 \\ 2 & n = 1 \\ 3 & n = 2 \\ 4 & n = 3 \\ 2G_{n-1}-2G_{n-3}+G_{n-4} & n\geq4 \end{cases}$$ How can I prove that $f(n) = n$...
2
votes
1answer
170 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
116 views

Loop Invariant summation

So I am stuck: I have this algorithm from which I need to find a loop invariant but I just can't get my head around it : ...
2
votes
1answer
343 views

Proving correctness of an iterative Fibonacci algorithm

One of the questions in the problem sets that I'm struggling in is this specific number that asks me to prove an iterative Fibonacci algorithm. The algorithm is written below: ...
2
votes
0answers
666 views

Finding the weakest precondition and invariant of while loop

I am trying to find the weakest precondition and invariant of this while loop. I have read and am trying to understand the concept of calculating preconditions based on postconditions. I was wondering ...
1
vote
3answers
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 ...
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 ...
1
vote
1answer
841 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
1k 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. ...
1
vote
1answer
50 views

Finding a strong loop invariant

Pseudocode: if n < 2 return false while n != 1 if n % 2 != 0 return false n = n/2 return true The loop will terminate when n is odd. If n =...
1
vote
1answer
305 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. ...
1
vote
1answer
15 views

How to understand out of bound in the following theoretical context?

Consider the following initialization step of loop invariant for merge procedure Initialization: Prior to the first iteration of the loop, we have $k=p$, so that the subarray $A[p .. k - 1]$ is ...
1
vote
1answer
75 views

Loop termination - Loop invariant

(x >= 0 && y >= 0) q = 0; r = x; while ( r >=y ) { r = r - y; q = q + 1; } (x = q*y +r) && (r >= 0) && (r < y) For ...
1
vote
1answer
55 views

How to create an algorithm when given the invariant

I am given the following invariant: Invariant The greatest $i$ keys of an Array are always in sorted order on the last $i$ indices of the Array. I am supposed to ...
1
vote
1answer
105 views

What is the loop invariant of the following function?

x = n; y = 0 while x >= b: x = x DIV b y = y + 1 return y This function takes in $n,b\in\mathbb{N}, n > 0, b > 1$, and returns $k\in\mathbb{N}$ ...
1
vote
2answers
293 views

Prove correctness of iterative LCM algorithm

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

Dealing with test condition '=' for a while loop when determining a bound function/loop variant

The following is the definition of what a bound function for a while loop must satisfy: The bound function is an integer-valued, total function of some of the inputs, variables and global data that ...
1
vote
1answer
93 views

Proving correctness of the Newton's Method for finding the square root of a number

I'm trying to prove the correctness of this simple square root calculation algorithm using SPARK: ...
1
vote
0answers
28 views

Does code motion/hoisting happen on if statements/branches? [closed]

Consider the following C code: for(int i=0; i<100000; i++) { if (operation == 0) { a[i] *= 2; } else { a[i] += 1; } } Would a real ...
1
vote
1answer
322 views

How to get Loop invariants to prove program is correct in Hoare logic

start off stating the definition of a loop invariant. It is a condition that must be true at the start of the loop and must be true after each iteration of the loop. I understand what it is but i have ...
1
vote
0answers
61 views

Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...
1
vote
0answers
696 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 $...
0
votes
2answers
140 views

Loop invariant for adding 2 arrays storing binary value of integer

Question: Given 2 arrays of size $n$, $A = \langle a_1,a_2,\dots,a_n \rangle$ and $B = \langle b_1,b_2,\dots,b_n\rangle$, where $A$ and $B$ store the binary value of an integer. Find $A + B$ and ...
0
votes
1answer
66 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\}$ ...
0
votes
1answer
61 views

Inference rules for deriving invariants in Hoare logic

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
0
votes
1answer
121 views

Loop invariant condition IsPrime program

I'm new to the concept of loop invariant and I'm trying to figure out the loop invariant for a program that returns if an integer is prime and, if not, one possible factorization. My intuition is that ...
0
votes
2answers
36 views

Deterministic Nonfinite Automaton - Longest Block of Ones

How to Think About Algorithms - Jeff Edmonds Exercise 2.2.2 The problem asks to find $\sum$, Q, δ, s, and F of this program if we see it as an automaton. Edmonds characterized this as deterministic ...
0
votes
1answer
51 views

Verification condition in case of array theory

As far as i can understand the problem of checking safety property, can be reduce to solving for inductive invariants in VC's and there is following parts to it: Generate VC's from the program. Solve ...
0
votes
1answer
98 views

What does the algorithm calculate?

We have the following ...