# Questions tagged [loop-invariants]

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

12 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 ...
0answers
245 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
670 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
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
104 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: ...
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 ...
0answers
711 views

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 ...