# Questions tagged [loop-invariants]

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

70 questions
Filter by
Sorted by
Tagged with
813 views

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

I am trying to mathematically prove that the following program is correct: ...
68 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\}$ ...
36 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.
64 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): ...
169 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 ...
40 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 ...
53 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 ...
106 views

### What does the algorithm calculate?

We have the following ...
62 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: ...
14 views

### How to write the invariants for one version of binary search insertion point (or leftmost entry) algorithm?

If we compare the binary search algorithm (leftmost or insertion point) on Wikipedia: Algorithm 1: ...
19 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: ...
38 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. ...
54 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--; } ...
118 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 , ...
45 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$ ...
28 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$ ...
49 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 ...
142 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 ...
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.