Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
2
votes
1answer
11k views

Proving greedy choice property of fractional knapsack

A typical way of proving the greedy choice property of the fractional knapsack problem is as follows: From Slide 5 of this link: Given: A set of items $I = \{I_1,I_2..I_n\}$ with weights $\{w_1,w_2 ....
5
votes
1answer
390 views

Question about the formal proof of the inorder traversing

In Don Knuth's famous series of books, The Art of Computer Programming, section 2.3.1, he describes an algorithm to traverse binary tree in inorder, making use of an auxiliary stack: T1 [Initialize....
0
votes
0answers
187 views

Prove a bisimulation relation

I need to prove a bisimulation relation on $CA_{\tau}(N)$ (communication algebra with tau-steps) and names $N$. It need to prove that $p!d.x||p?d.y$ is bisimular with $p!d.(x||p?d.y)+p?d.(p!d.x||y)$ ...
1
vote
1answer
81 views

For Djikstra's algorithm, why are we surely done if we update all edges $|V|-1$ times?

Apparently, if we use Djikstra's algorithm to find the shortest path between the root node and all other nodes in a weighted graph with no negative cycles, we are done after updating the distance of ...
1
vote
0answers
2k views

Insertion sort Proof by Induction

I am reading Algorithm design manual by Skiena. It gives proof of Insertion sort by Induction. I am giving the proof described in the below. Consider the correctness of insertion sort, which we ...
0
votes
1answer
699 views

Proving correctness of the algorithm for convex polygon minimum cost triangulation

I have read many solutions for the minimum cost of triangulation problem and intuitively get the idea , however I am struggling to figure out how to prove it formally. I kind of feel that it has to be ...
1
vote
1answer
491 views

While proving optimality of the A* algorithm, why can we change graphs?

In the original paper of A* algorithm, A Formal Basis for the Heuristic Determination of Minimum Cost Paths, the author proved the optimality of A* in Theorem 2, page 105. However, I cannot ...
7
votes
1answer
2k views

A procedure for Topological sort, proof for its correctness

Definition: A preserved invariant of a state machine is a predicate, $P$, on states, such that whenever $P(q)$ is true of a state, $q$, and $q \rightarrow r$ for some state, $r$, then $P(r)$ holds. ...
1
vote
3answers
179 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 ...
1
vote
3answers
952 views

A* optimality of the expanded node

Suppose I have a admissible and consistent heuristic. Is it true, that when I expand a node, I have guaranteed that the path I found to this node is optimal? Look at this pseudocode from wikipedia: ...
0
votes
1answer
313 views

Can GDB debug itself?

Can GDB be run on itself? How or why not? I see something about it http://www.math.utah.edu/docs/info/gdbint_3.html But GDB might not be written in a language that it can debug?
3
votes
1answer
323 views

The use of multiset ordering in proving termination

Based on the definition of a multiset and the information in this paper, why do we use multisets in proving the termination of a program? Is not the well-founded order enough?
1
vote
3answers
8k views

DFS - Proof of Correctness

I'm currently studying the book "Introduction to Algorithms - Cormen". Although a proof of correctness for the BFS algorithm is given, there isn't one any for the DFS in the book. So I was courious ...
0
votes
0answers
67 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 ...
1
vote
3answers
2k 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 not ...
2
votes
1answer
265 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 ...
3
votes
1answer
1k views

Loop invariants?

...
6
votes
1answer
339 views

Will this algorithm terminate on any input?

One can compress data with straight-line grammars. An algorithm that employs this technique is called Sequitur. If I understood correctly, Sequitur basically starts with one rule representing the ...
7
votes
1answer
4k views

Prove correctness of recursive multiplication algorithm

I'm in a first year discrete math course and we started algorithms. I created a recursive algorithm to multiply two numbers together: ...
2
votes
2answers
168 views

Rigorous proof against pseudorandom generator

I am trying to teach myself the principles of cryptograhpy, and want to solve the following question: Let G be the algorithm that takes an input x = (x1, . . . , xn) from {0, 1} n (so each xi ∈ {...
5
votes
1answer
925 views

How to prove that BFS directed-graph traversal algorithm terminates?

How to prove that BFS directed-graph traversal algorithm terminates? (I copy the pseudocode from here) Input: A graph G and a root v of G. ...
5
votes
1answer
936 views

How to prove that the pre-order tree traversal algorithm terminates?

I see structural induction the usual way for proving an algorithm's termination property, but it's not that easy to prove by means of induction on a tree algorithm. Now I am struggling on proving that ...
4
votes
1answer
533 views

Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...
6
votes
0answers
1k views

A variation in Ford-Fulkerson algorithm

Suppose that we redefine the residual network to disallow edges into $s$. Argue that the procedure FORD-FULKERSON still correctly computes a maximum flow. I was thinking that when we augment a path ...
10
votes
1answer
713 views

Micro-optimisation for edit distance computation: is it valid?

On Wikipedia, an implementation for the bottom-up dynamic programming scheme for the edit distance is given. It does not follow the definition completely; inner cells are computed thus: ...
24
votes
1answer
5k views

How to prove correctness of a shuffle algorithm?

I have two ways of producing a list of items in a random order and would like to determine if they are equally fair (unbiased). The first method I use is to construct the entire list of elements and ...
7
votes
2answers
2k 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: <...
10
votes
2answers
978 views

How is the loop invariant obtained in this square root bound finding algorithm?

Originally on math.SE but unanswered there. Consider the following algorithm. ...