# Questions tagged [loop-invariants]

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

63 questions
Filter by
Sorted by
Tagged with
1answer
13 views

### Loop invariant initialisation confusion

Consider the algorithm LastMatch below, which returns the offset (shift) of the last occurrence of the pattern P in text T, or -1 if P does not occur in T: ...
0answers
33 views

### Proof that this sorting algorithm sorts the input

I'm given this "sorting" algorithm and now I'm supposed to prove, that if given an array of integers of length $n$, sort(A,0,n-1) will sort it. ...
1answer
40 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 ...
1answer
53 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$...
1answer
37 views

### Loop Invariant Code Motion - am I missing something?

I've been implementing LICM for a project, and came upon a strange observation. Let's say we have a loop int i = 10; while (i > 0) { a = 2; i--; } ...
1answer
45 views

### Loop-Invariant for a program fragment

Q) Consider the following program fragment: var x,y:integer; x:=1; y:=0; while y < x do begin x:=2∗x; y:=y+1; end; For the above fragment , ...
1answer
29 views

### Finding invariant when detecting a cycle

Let consider a connected graph $G = (V, E)$ which is not oriented. One way to detect a cycle in such a graph is : Create an array : seen of size $\mid V \mid$ with seen[i] = false for all $i$ ...
1answer
107 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: ...
1answer
43 views

### Find an invariant in the minimum algorithm

I have the following simple algorithm to find the smallest element of an array $A$ of numbers: ...
2answers
193 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: ...
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 ...
0answers
27 views

### Equivalent Algorithm with Sharman Morrison inversion

I am trying to invert a matrix using Woodbury identity. The inversion using Cholesky decomposition has the following pseudo-code: For $t=1,2,...$ $(1)\;\; \text{Read}\;x_t\in\mathbb{R}^n$ ...
0answers
32 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 ...
1answer
120 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 : ...
1answer
51 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 =...
1answer
161 views

### Is Loop Invariant Proof a form of Induction?

As far as I see, what computer scientists refer to as loop invariant proofs are exact replicas of induction proof. Is it true? Can I state that loop invariant proof implies an induction? Is there a ...
2answers
171 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 ...
1answer
79 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 ...
1answer
119 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. ...
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): ...
0answers
45 views

### Loop invariant for

The programme returns the number of digits of an integer $n>0$. I still have some difficulties to understand the difference between the loop invariant condition and what the loop should actually ...
1answer
89 views

### Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
1answer
128 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 ...
1answer
347 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: ...
0answers
122 views

### Counting the number of occurences - loop invariant

I'm trying to come up with loop invariant for the following program. k = a m = 1 p = 1 while p < n: if a[p] == k: m += 1 p += 1 return m I ...
1answer
340 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 ...
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 ...
0answers
246 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 ...
0answers
62 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 ...
1answer
58 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 ...
1answer
106 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}$ ...
2answers
150 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 ...
2answers
263 views

### Loop invariant for a while loop

I need help understanding why the two statements I have underlined with red are correct. I am confused as to how we can get $n + 1$. And how $i \le n$ is true when it says $i < n$ in the while.
1answer
506 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. ...
1answer
264 views

### Finding a loop invariant

the following pseudo code returns the nth Fibonacci number: ...
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 ...
1answer
794 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: ...
0answers
671 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 ...
1answer
99 views

### What does the algorithm calculate?

We have the following ...
0answers
715 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 \$...
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 ...
2answers
294 views

### Prove correctness of iterative LCM algorithm

I have been trying to prove the following algorithm, without success. Here is the C-Style pseudocode: ...
1answer
171 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 ...
1answer
812 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 ...
3answers
1k views

### Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
1answer
714 views

### Proving correctness of a loop that calculates the sum of array

I am trying to mathematically prove that the following program is correct: ...
1answer
854 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: ...
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. ...
2answers
630 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 ...
2answers
627 views

### Understanding Log(n) Loop Invariant

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