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
0 votes
1 answer
98 views

Any hints about loop invariant of weird loop?

I have this tiny program for finding largest prime divisor (taken from Code Review Stackexchange and written by user Altinak: https://codereview.stackexchange.com/a/74792): Here is my try to write it ...
Lessness Randomness's user avatar
0 votes
1 answer
2k views

MergeSort's merge function loop invariant

I am reading a proof of correctness for the MergeSort Algorithm. This is the code for the MergeSort and the Merge function: The correctness of the MergeSort function is easy to prove since the two <...
mateleco's user avatar
  • 108
0 votes
1 answer
129 views

Struggling to find loop invariant in power function

I am struggling to find a good loop invariant for the following function, which returns a^b where a is a real number and b is a natural number: ...
Jeremy's user avatar
  • 3
0 votes
1 answer
484 views

Finding the loop invariant for Array Reversal

I've been assigned to find the loop invariant for the following code: ...
ifiht's user avatar
  • 103
0 votes
1 answer
82 views

Why is there a 'true' statement as precondition in the following loop invariant

Precondition: true int i = 0; while (i < a.length && a[i] != x) { i++; } Postcondition: (∀ j : 0 ≤ j < i : a[j] ≠ x) ⋀ (i = a.length ∨ a[i] = x) } As I read it, the program has no ...
Rubus's user avatar
  • 121
1 vote
1 answer
58 views

Are there invariants in text processing problems?

I have read that when programming it is good to identify relations -- invariants -- that should hold true throughout the program, and it is good to insert assertions throughout the code to check that ...
Roger Costello's user avatar
2 votes
1 answer
133 views

What loop invariant can be used for this loop? (Algorithm to check if a sequence is stack permutable)

I've written a function that gets a permutation and checks if that permutation can be reached using a stack from an input sequence which is <1,2,3,...,n>. (we take elements from left) For ...
Pwaol's user avatar
  • 164
0 votes
1 answer
56 views

Proving loop invariant for a possibly nonterminating while loop

I started studying through Aho, Ullman - Foundations of Computer Science as a free time exercise. In the second chapter about loop invariants and inductive proofs, there is a starred exercise. ...
meguli's user avatar
  • 293
0 votes
2 answers
615 views

Proving the correctness of an algorithm

What is the logic behind using a loop invariant proof for proving the correctness of an algorithm? How is it proved that using the loop invariant proof indeed proves the correctness of a loop?
Kashish's user avatar
0 votes
1 answer
65 views

What could be a good loop invariant for this?

I am currently new and learning about loop invariants. I have come across this pseudocode where the goal is to shift the elements inside an array with N size in a clockwise direction by K steps. ...
fynn's user avatar
  • 3
1 vote
1 answer
88 views

Does loop invariant has nothing to do with termination?

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, which ...
Harleen Kaur's user avatar
2 votes
1 answer
378 views

Proof of algorithm correctness

I am studying about algorithm correctness and have enctountered this problem. ...
Exzone's user avatar
  • 235
1 vote
0 answers
2k views

loop invariant of selection sort algorithm

I am asked to write an C code Selection Sort algorithm and use loop invariant to show its correctness. ...
Alparslan's user avatar
  • 113
1 vote
1 answer
154 views

What is loop invariant for this loop?

As far as i understand all loops have a loop invariants. My understanding is that loop invariant is an argument that is true at the beginning of the loop block as well as at the end of the loop. For ...
Oleksandr Papchenko's user avatar
0 votes
1 answer
132 views

understanding loop invariants

I have a bit of experience with loop invariants but I'm not really clear on them. I'm trying to learn them through an Algorithm I have. ...
lexemto10's user avatar
1 vote
2 answers
1k views

quicksort invariant 3 conditions with loop invariant

in studying Quicksort using the book "Introduction to Algorithms" by Cormen, Leiserson, Rivest and Stein, they describe in order to show correctness, an invariant must hold for the 3 stages of the ...
Katie Melosto's user avatar
1 vote
1 answer
152 views

Hoare Logic for Factorial

I came across this hoare logic for factorials but I don't quite understand it. We multiply F and X but we're not adding up all values of F so how do we get the sum/factorial at the end? Precondition: ...
x89's user avatar
  • 167
1 vote
0 answers
188 views

Loop invariant of a search algorithm

I have to come up with a proof of correctness of the following algorithm: GuardedSearch(A; v) Input: an array A of n numbers and a number v Output: an index i such that A[i] = v, or NotFound if no ...
MaximeB's user avatar
  • 33
5 votes
1 answer
100 views

Is there a model of ZF¬C where some program always terminates but has no loop variant?

Wikipedia has a proof that every loop that terminates has a loop variant—a well-founded relation on the state space such that each iteration of the loop results in a state that is less than the ...
Aaron Rotenberg's user avatar
0 votes
1 answer
56 views

I cannot find an invariant for the following program

I have the following: (|$y=0; x=c$|) while(x > 0){y=y+a; x=x-1;} (|$y= a*c$|) This seems like a fairly simple program and I can intuitively tell that the post ...
KetDog's user avatar
  • 157
2 votes
2 answers
406 views

Implementing Tarjan's strongly connected components algorithm in a language without exceptions or undefined behavior

I asked this question on Stack Overflow, but I have not obtained an actual answer to the question. Tarjan's strongly connected components algorithm is stunningly beautiful, and inexpressible in a ...
isekaijin's user avatar
  • 405
0 votes
1 answer
47 views

How do I "apply" a loop invariant?

A homework problem I have asks that I "state" a loop invariant, then "prove" it, then "apply" it. I get state and prove, but my textbook doesn't explicitly state how to "apply" a loop invariant.
Ace Zhang's user avatar
1 vote
1 answer
87 views

When are invariants true inside of a loop?

I am new to the idea of invariants and hope to find more information about it. It can make an algorithm or loop show a high level of certainty / confidence that the code is correct, such as in the ...
nonopolarity's user avatar
0 votes
1 answer
40 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: ...
Data's user avatar
  • 215
1 vote
3 answers
426 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 ...
SeesSound's user avatar
  • 155
2 votes
1 answer
92 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$...
AdillioN's user avatar
1 vote
1 answer
126 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--; } ...
aolo2's user avatar
  • 13
0 votes
1 answer
809 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 , ...
ankit's user avatar
  • 169
0 votes
1 answer
172 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$ ...
1597846254899's user avatar
1 vote
2 answers
303 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: ...
Alex's user avatar
  • 11
0 votes
1 answer
514 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: ...
user100778's user avatar
1 vote
2 answers
1k 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: ...
user avatar
1 vote
1 answer
19 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 ...
hanugm's user avatar
  • 495
0 votes
0 answers
36 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$ ...
Waqas's user avatar
  • 101
1 vote
0 answers
38 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 ...
cannon's user avatar
  • 11
2 votes
1 answer
383 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 : ...
Sami's user avatar
  • 35
1 vote
1 answer
221 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 =...
weztex's user avatar
  • 13
2 votes
1 answer
2k 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 ...
Ninja Bug's user avatar
  • 249
3 votes
2 answers
401 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 ...
zack's user avatar
  • 196
1 vote
1 answer
202 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 ...
user avatar
2 votes
1 answer
348 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. ...
the_martian's user avatar
0 votes
1 answer
82 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): ...
hengxin's user avatar
  • 9,501
0 votes
0 answers
141 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 ...
FunnyBuzer's user avatar
4 votes
1 answer
113 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
hengxin's user avatar
  • 9,501
0 votes
1 answer
622 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 ...
FunnyBuzer's user avatar
2 votes
1 answer
1k 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: ...
Jessie's user avatar
  • 123
0 votes
0 answers
431 views

Counting the number of occurences - loop invariant

I'm trying to come up with loop invariant for the following program. k = a[0] m = 1 p = 1 while p < n: if a[p] == k: m += 1 p += 1 return m I ...
Paweł's user avatar
  • 9
1 vote
1 answer
912 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 ...
Cathal Brady's user avatar
0 votes
2 answers
50 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 ...
namesake22's user avatar
3 votes
0 answers
753 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 ...
Zooky's user avatar
  • 131