# Tagged Questions

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

21 views

### while loop program corectness - invariant and hoare logic

Could someone verify my proof in hoare logic ? It is about invariant for loop while, look: ...
82 views

### How to use the concept of loop invariant to reduce errors in loops?

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Here is an small example ...
71 views

### How to find loop invariant from weakest precondition?

Consider this code: Precondition: Postcondition: rv == i <==> ∃i, 0 ≤ i ≤ a.length-1, a[i] == key ...
207 views

### Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
54 views

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

I am trying to mathematically prove that the following program is correct: ...
107 views

### Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct? I'm asked to prove (using Hoare Logic) that the following program is valid: ...
75 views

### Trouble finding loop invariant for this while loop

I'm having trouble coming up with an invariant for proving partial correctness of this function. ...
140 views

### Loop variant for a while loop that occasionally doesn't decrease?

I'm working on practice problems for a test I have, and every example of loop variant decreased with every iteration of the loop. On this one, the values remain the same when a < b. My attempts ...
128 views

### Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
225 views

### Finding a good loop invariant

I want to prove that the following program is correct. The code takes an array i of length N and a number ...
96 views

### Loop invariant: decreasing a variable and swapping it

As an example exercise, we were asked to find the loop invariant for this bit of code. ...
164 views

### Loop-invariant code motion with unsafe operations

There are well-known algorithms LICM, and they work well. Unfortunately, there are certain cases when these optimizations can cause runtime failures with code that was initially correct. Consider the ...
2k views

### Proof of Program Correctness - Loop Invariants

I've been reading a book on using loop invariants and induction to prove program correctness. Then I came across the following program which got me thinking... Specification for ...
53 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\}$ ...
116 views

### Loop Invariants as Tautologies

Would it be correct to characterize loop invariants as a type of tautology? I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop ...
45 views

### loop invariant proof [duplicate]

Possible Duplicate: Proof of linear search? I'm reading the MIT Press, Introduction to Algorithms textbook 3rd edition, and I am a bit confused by an exercise. 2.1-3 Consider the searching ...
1k views

### Proof of linear search?

Consider the searching problem: Input: A sequence of $n$ numbers $A=(a_1, a_2, \ldots , a_n)$ and a value $v$. Output: An index $i$ such that $v = a_i$ or the special value NIL if $v$ does ...
204 views

### Invariant Proof of For Loops?

From CLRS (third edition, page 19), there is a footnote: When the loop is a for loop, the moment at which we check the loop invariant just prior to the first iteration is immediately after the ...
265 views

### Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...
864 views

### Invariant For Nested Loop in Matrix Multiplication Program

I'm making a graduate thesis about proving correctness of program for multiplying 2 matrices using Hoare logic. For doing this, I need to generate the invariant for nested loop for this program: <...
I have developed the following pseudocode for the sum of pairs problem: Given an array $A$ of integers and an integer $b$, return YES if there are positions $i,j$ in $A$ with $A[i] + A[j] = b$, NO ...