Questions that ask for or about correctness proofs of algorithms.

learn more… | top users | synonyms

0
votes
0answers
16 views

Intermediate predicates in partial correctness verification with Hoare triples

I am trying to prove partial correctness for this algorithm, but I don't know if I am following a correct procedure, if there exists any, in order to find intermediate postconditions after ...
2
votes
2answers
49 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
0
votes
0answers
26 views

Proving a dynamic programming recurrence for coin exchange correct

Suppose I have n kinds of coins c_1, c_2, ..., c_n. I'm I given: S, sum of money I should construct with minimum number of coins. I came into the following formula: T(n,S) = T(n-1,S) if c_n > S ...
0
votes
1answer
29 views

prove sufficient number of comparisons for the merge problem

It is given two subsequences. Their length are following: $2$ and $5$. I can show that lower bound of comparisons is $5$. My problem is that I can't show that $5$ is sufficient number of comparisons ...
3
votes
3answers
1k views

Why does this sort algorithm work?

The following O(n^2) sorting algorithm works but I can't figure out why. ...
-1
votes
1answer
19 views

Proving correctness of a recursive algorithm using induction

For the program mean(A,n) if n = 1 then return A[n] else return A[n]/n+mean(A,n-1)*(n-1)/n end Show that if the recursive call to ...
-2
votes
1answer
56 views

Using dynamic programming to find the number ofl increasing subsequences [closed]

I got this question today and I'm nowhere near the solution, Given a sequence of real numbers (X1, X2, ..,Xn). write an algorithm as efficient there is, that finds the number of strictly increasing ...
3
votes
1answer
75 views

Greedy algorithm correctness proof for “Elegant Permuted Sum” (UVa 11158)

Given a sequence of $2 \leq n \leq 50$ numbers $s = (s_1,s_2,...,s_n)$, find a permutation $a = (a_1,a_2,...,a_n)$ of $s$ such that $$\sum_{i=1}^{n-1} |a_i - a_{i+1}|$$ is maximized. I found many ...
0
votes
2answers
63 views

How does this Turing machine accept $a^n b^n$?

I'm reading this tutorial from the University of Illinois about Turing Machines, and I don't understand something. They give a pseudocode algorithm for an machine that accepts strings from the ...
0
votes
1answer
84 views

Complete examples of program correctness proofs

Does anyone have any complete example of a proof of program correctness? I'm talking about something that includes the usual predicate, base case, inductive hypothesis, and inductive step. But also ...
0
votes
1answer
33 views

Which element is at its final position after the partitioning step in Quicksort?

In Algorithms, 4th Edition, I read that after the partitioning step one element is in its final position. The entry a[j] is in its final place in the array, for some j. No entry in a[lo] ...
2
votes
1answer
148 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 ...
2
votes
1answer
89 views

Updating an MST $T$ when the weight of an edge not in $T$ is decreased

Given an undirected, connected, weighted graph $G = (V,E,w)$ where $w$ is the weight function $w: E \to \mathbb{R}$ and a minimum spanning tree (MST) $T$ of $G$. Now we decrease the weight by $k$ ...
-1
votes
1answer
115 views

Prove that Ford-Fulkerson can decide if there is more than one min cuts

Probelm: Deciding whether a network flow graph has more than one min cut. Optimal running time: O(V^2*E). I trying to prove the correctness of the next algorithm: run Dinitz to find max-flow and ...
3
votes
0answers
29 views

How is Chinese Remainder Theorem used in the proof of correctness for RSA

Question At the very end of (most) proofs of RSA's correctness we have something like $$m^{ed}\equiv m\pmod p$$ $$m^{ed}\equiv m\pmod q$$ Therefore by the Chinese Remainder Theorem (CRT) ...
0
votes
2answers
73 views

Counter example to graph coloring heuristic using BFS

I am considering the following heuristic for the graph coloring problem (i.e. to color a graph $G$ using a minimal number of colors so that no two adjacent vertices have the same color): Explore ...
3
votes
1answer
34 views

Seemingly non sequitur in proof

I'm trying to understand a small proof in an article about computing lumpability on Markov chains. There is a small detail that I cannot understand, i.e. I don't think it follows from the argument. ...
0
votes
1answer
86 views

People crossing a bridge (a proof for a greedy algorithm)

The problem Some people are crossing a bridge. Each one takes a different time to pass. Assume the people are sorted by their passing time increasingly. These are the conditions of crossing the ...
0
votes
2answers
227 views

Why do these recurrences determine the number of ways of tiling a 3xN rectangle with 2x1 dominoes?

http://www.algorithmist.com/index.php/UVa_10918 The above link is a solution to UVa 10918 Problem. The problem is based on Dynamic Programming. I am not able to understand this approach to the ...
0
votes
0answers
23 views

Proving the correctness of the CKMS algorithm for biased quantiles

I'm trying to prove the correctness of my implementation of the CKMS algorithm from "Effective Computation of Biased Quantiles over Data Streams" and I'm having trouble showing that my implementation ...
1
vote
1answer
337 views

provability of while loop vs for loop [closed]

I'm abit afraid to ask this question here seeing as I asked it on programmers SE already, the thing is I think the question is more about the underlying theory than the use in practice (or call it ...
1
vote
2answers
51 views

Given the “programs as proofs” isomorphism, how do we know that the program isn't lying?

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the ...
4
votes
0answers
190 views

Suurballe's Algorithm: Proof of Correctness

I was reading about Suurballe's algorithm on Wikipedia, for the shortest edge-disjoint paths problem, i.e. given nodes $s$ and $t$ finding a pair of paths between these nodes, whose accumulated weight ...
17
votes
2answers
1k views

Are there programs that never halt and have no non-termination proof?

Like black holes in computer science. We can only know they exist but when we have one of them we will never know it's one of them.
4
votes
1answer
321 views

Is there a flaw in this Wikipedia proof of cycle property of Minimum Spanning Tree?

On wikipedia, there is a proof for the cycle property of the Minimum Spanning Tree as follows: Cycle Property: For any cycle C in the graph, if the weight of an edge e of C is larger than the ...
1
vote
0answers
62 views

Proof of Randomized Self-Adjusting Binary Search Tree

I developed a randomized self-adjusting binary search tree years ago, which I called a shuffle tree, but was unable to ever have it published because my proofs were rejected (with little explanation). ...
2
votes
2answers
120 views

How to go about proving an algorithm correct?

The algorithm (called as rmax(1,n)) finds the maximum of a list of numbers contained in an array S[1..n]. ...
3
votes
2answers
345 views

Binary Indexed Trees: Why does i & -i work?

I already read this related question on the intuition behind binary indexed trees, and while the answer explains how the tree structure works, it does not really explain how this correlates back to ...
0
votes
1answer
71 views

Understanding a proof in the sweep line algorithm when finding all line segment intersections

You have a set of line segments and you want to find all intersections. First sweep line approach: Use a priority queue Q for the events as they come, where each ...
3
votes
3answers
586 views

Rigorous Proof of Insertion Sort

Currently I self study CLRS book (Outside of any course, so I got no access to an instructor) And I am stuck proving Insertion Sort, The proof in CLRS book is not so formal. Here's the algorithm: ...
0
votes
0answers
92 views

stuck on proving the optimality of a greedy algorithm [closed]

I'm Ph.D. student doing research in wireless networks. My past projects are more oriented to systems than theory. For my current project, I devised a greedy algorithm for an optimization problem. ...
1
vote
1answer
98 views

Proving correctness of an AVL-Tree colouring algorithm

I came up with the following recursive algorithm to colour the nodes of an AVL tree so that the resulting tree is red-black. The logic is that the algorithm first colours the root and, recursively, ...
5
votes
1answer
259 views

Proving optimality of a dynamic programming algorithm

We have a string $s$ containing $n \leq 100$ bits. The move we can make on it is erasing from $s$ some substring $x$, but only if $x$ is directly preceded by $x^R$, where $x^R$ means string $x$ ...
0
votes
2answers
105 views

How to show that this algorithm for evaluating polynomials works?

I'm having trouble showing how to solve this problem in particular the part where it asks "To Show that the following pseudo-code fragment finds the value of the polynomial..." How do I exactly show ...
0
votes
2answers
90 views

Hoare Calculus Incorrect Assignment Axiom

I'm currently preparing for an exam and recently came across the following exercise and would like to know whether my solution would be correct. Exercise: Prove that the following axiom is not ...
52
votes
12answers
5k views

How to fool the “try some test cases” heuristic: Algorithms that appear correct, but are actually incorrect

To try to test whether an algorithm for some problem is correct, the usual starting point is to try running the algorithm by hand on a number of simple test cases -- try it on a few example problem ...
1
vote
2answers
821 views

Proof of an Optimal substructure in Dynammic Programming?

Could someone please explain how exactly the proof of optimal substructure property in dynamic programing problems works?, they usually say that " let's say the global optimal solution is A, and B is ...
-2
votes
1answer
37 views

why negative cycle exists if we can relax the edges one more time after running the Bellman Ford Algorithm

We know Bellman Ford is an algorithm to find the negative cycle. And here is the algorithm for Bellman Ford Input: Given a graph G(V,E) and w(e) is weight Output: Return Yes if negative cycle exists. ...
0
votes
1answer
116 views

Concept used in the proof [closed]

In the paper "Resolution for Quantified Boolean Formulas", I am unable to understand the proof of theorem 3.4. Please help me with the basic concept used on page 4: The concept that I am referring ...
1
vote
0answers
28 views

Conjecture about a matrix column swapping challenge problem

So here is the challenge problem statement: https://icpcarchive.ecs.baylor.edu/index.php?option=com_onlinejudge&Itemid=8&page=show_problem&problem=1512 Basically, given a 0/1 matrix, you ...
8
votes
6answers
248 views

Could program verification techniques prevent bugs of the genre of Heartbleed from occurring?

On the matter of the Heartbleed bug, Bruce Schneier wrote in his Crypto-Gram of 15th April: '"Catastrophic" is the right word. On the scale of 1 to 10, this is an 11.' I read several years ago that a ...
1
vote
2answers
525 views

Correctness proof of greedy algorithm for 0-1 knapsack problem

We have a 0-1 knapsack in which the increasing order of items by weight is the same as the decreasing order of items by value. Design a greedy algorithm and prove that the greedy choice guarantees an ...
3
votes
0answers
109 views

Maximum Weight Independent Set in Circular-Arc Graphs (Proof of A Lemma)

I am reading the paper: "Maximum Weight Independent Set Of Circular-Arc Graphs and It's Applications" (http://link.springer.com/article/10.1007%2FBF02832044). And I had a question regarding the proof ...
1
vote
1answer
55 views

Proving the correctness of an algorithm, which computes the connectivity of a directed graph

Let $G=(V,E)$ be a directed graph. The connectivity of a graph is the defined as the cardinality of a smallest separator of $G$. A separator of $G$ is a subset $U$ of $V$, such that $G-U$ is not ...
2
votes
1answer
273 views

How can we minimize the total distance of cross pairs in an array

Suppose we had 2 arrays of the same size with positive numbers and we wanted to pair up the elements of each array such that the total difference between the pairs is minimized. The first thought ...
-1
votes
2answers
371 views

Proof of Correctness of Prim's algorithm [duplicate]

what is the reason for the correctness proof of Prim's Algorithm for the undirected case cannot carry over to the directed case? Is it because of after any number of steps, $S$ might not be in a sub ...
3
votes
1answer
223 views

Viterbi algorithm recursive justification

I have a question regarding recursion in Viterbi algorithm. Define $\pi(k; u; v)$ which is the maximum probability for any sequence of length $k$, ending in the tag bigram $(u; v)$. The base case ...
3
votes
2answers
112 views

Is there a proof of the recursive algorithm for generating all permutations of a sequence?

For clarity, I attach below a concise implementation of the algorithm in Python. I understand that it checks all possible element swaps, but I don't see how that necessarily means that all possible ...
0
votes
1answer
76 views

What is wrong in this proof? [closed]

I stumbled upon this wikipage that has got this proof : I rechecked sum rule of differentiation. And i can not understand where is this wrong. Any Tips ? I think that the second line x^2 = x + ...
0
votes
1answer
95 views

trouble with bijection definition [closed]

I have a bijection problem that I cannot get my head around. It goes like this: let f: A -> B and g: B -> C be functions such that g o f is a bijection. Prove that f must be one-to-one and that g ...