Questions tagged [loop-invariants]

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

13 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
3
votes
0answers
388 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
0answers
712 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
0answers
76 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 ...
1
vote
1answer
175 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
80 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
828 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
0answers
23 views

How to determinne the loop invariant?

The following code returns the number of trailing zeros of an integer x (number of 0s at the end of the decimal number representation of x). I had to find its loop invariant, which is ...
0
votes
0answers
15 views

Finding bound function of loop invariant

In Programming in the 1990s, by Edward Cohen, the author gives an example of a bound function. For example, if we have $B \equiv 10 - n$ where $n = 0$, say, then $B$ will eventually be falsified if ...
0
votes
0answers
22 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: ...
0
votes
1answer
60 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$ ...
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$ ...
0
votes
0answers
53 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 ...
0
votes
0answers
196 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 ...