# 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
320 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 ...
693 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 ...
61 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 ...
145 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: ...
76 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 ...