Questions tagged [loop-invariants]
Properties that hold before and after every execution of a loop. Used to prove correctness of algorithms.
76
questions
1
vote
1answer
41 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 ...
1
vote
1answer
76 views
Proof of algorithm correctness
I am studying about algorithm correctness and have enctountered this problem.
...
1
vote
0answers
153 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.
...
1
vote
1answer
69 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 ...
0
votes
1answer
24 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.
...
1
vote
2answers
91 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 ...
1
vote
1answer
44 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: ...
1
vote
0answers
131 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 ...
5
votes
1answer
75 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 ...
0
votes
1answer
34 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 ...
2
votes
2answers
260 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 ...
0
votes
1answer
41 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.
1
vote
1answer
38 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 ...
0
votes
1answer
28 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:
...
0
votes
0answers
44 views
Proof that this sorting algorithm sorts the input [duplicate]
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.
...
1
vote
3answers
220 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 ...
2
votes
1answer
64 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$...
0
votes
1answer
75 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--;
}
...
0
votes
1answer
341 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 , ...
0
votes
1answer
95 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$
...
1
vote
1answer
209 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:
...
0
votes
1answer
267 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:
...
1
vote
2answers
734 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:
...
1
vote
1answer
16 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 ...
0
votes
0answers
29 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$ ...
1
vote
0answers
37 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 ...
2
votes
1answer
224 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 :
...
1
vote
1answer
129 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 =...
2
votes
1answer
825 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 ...
3
votes
2answers
249 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 ...
1
vote
1answer
138 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 ...
2
votes
1answer
228 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.
...
0
votes
1answer
71 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
0answers
65 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 ...
4
votes
1answer
102 views
Developing invariants for comparing two strings
The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):
...
0
votes
1answer
403 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 ...
2
votes
1answer
771 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:
...
0
votes
0answers
297 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 ...
1
vote
1answer
631 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 ...
0
votes
2answers
42 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 ...
3
votes
0answers
506 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 ...
1
vote
0answers
91 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
1answer
85 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
142 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}$ ...
0
votes
2answers
274 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 ...
-2
votes
2answers
333 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.
4
votes
2answers
817 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.
...
2
votes
1answer
371 views
0
votes
1answer
55 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 ...
2
votes
1answer
906 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:
...
