A message from our CEO about the future of Stack Overflow and Stack Exchange. Read now.

Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
3
votes
1answer
759 views

Proof for Minimum number of insertions to convert a string to a palindrome

For the problem "Find the minimum number of insertions to convert a string $S$ to a palindrome", a recurrence relation usually given is: $$ c[i,j] = \begin{cases} c[i+1,j-1] & \text{if } S[i] = S[...
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: ...
1
vote
2answers
303 views

Can we enumerate provably non-terminating functions?

In trying to understand the Halting Problem better, I am trying to come up with classes of provably non-terminating programs. For example, any program (including input) which leads to a finite-...
1
vote
5answers
505 views

Correctness of the greedy algorithm

I am trying to solve the following problem: Given a matrix which consists of only 0's and 1's. Considering the matrix as a metal sheet, we need to "cut-out" square blocks of sizes 2x2 consisting of ...
1
vote
1answer
928 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: ...
6
votes
2answers
801 views

Correctness of Freivald algorithm for checking matrix multiplication, why is the probability of checking $AB \neq C$ at least 1/2?

I am going to consider Freivald's algorithm in the field mod 2. So in this algorithm we want to check wether $$AB = C$$ and be correct with high probability. The algorithm choose a random $r$ n-...
-2
votes
1answer
215 views

An algorithm for vertex cover

Let $G = (V,E) $ and let be $T \subseteq V$ . $T$ is called vertex cover if each edge of the graph is incident to at least one vertex of $T$ . Let be the following decisional problem : $PROBLEM$ ...
3
votes
1answer
800 views

If we sort a table column-wise and then row-wise why the table is still sorted column-wise?

Say we have a $n \times n$ table which elements are sorted column-wise, for example: $$ \left( \begin{array}{ccc} 2 & 4 & 1 \\ 3 & 5 & 6 \\ 7 & 9 & 8 \end{array} \right) $$ ...
1
vote
1answer
258 views

Homomorphism Languages

Let $h$ be a homomorphism and let $L$ be a language. Writing ${}^*$ for Kleene star, I want to show that $(h^{-1}(L))^* \neq h^{-1}(L^*)$. Can I prove this just by showing that we can have $h^{-1}(...
4
votes
1answer
61 views

Inference rule with two conclusions or rather inverse function application

I want to express a simple correctness theorem for a term-desugaring function $\Delta$. The goal is to express that if the evaluation of a desugared term yields a value, this value is the desugared ...
0
votes
0answers
317 views

Proving a dynamic programming recurrence for coin exchange correct

Suppose I have $n$ kinds of coins $c_1, c_2, \dots, c_n$. I'm given: $S$, an amount of money I should construct with minimum number of coins. I came into the following formula: $$ T(n,S) = \begin{...
4
votes
1answer
847 views

Minimizing inversions in an array with a single swap

This was asked in the (very) recently concluded Hackerrank Worldcup. Paraphrased: Given a permutation $a$ of integers from $1$ to $N$, how can I minimize the number of inversions by a single swap ...
1
vote
2answers
215 views

How to prove if an algorithm is reentrant?

I think, maybe some formalism could exist for the task which makes it significantly easier. My problem to solve is that I invented a reentrant algorithm for a task. It is relative simple (its pure ...
0
votes
1answer
1k views

Algorithm for constructing BST from post-order traversal

Given a post-order traversal of Binary Search tree with $k$ nodes, find an algorithm that constructs the BST. My Algortihm Let $n$ represent the next element to be inserted. Let $P(y)$ ...
9
votes
3answers
1k views

Is it possible to prove thread safety?

Given a program consisting of variables and instructions which modify these variables, and a synchronization primitive (a monitor, mutex, java's synchronized or C#'s lock), is it possible to prove ...
0
votes
1answer
105 views

Proving equality between foldl recursive and iterative fold

Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative. I am looking for an algebraic proof that the two definitions are equal ideally ...
5
votes
2answers
8k views

Proof of an Optimal substructure in Dynammic Programming?

Could someone please explain how exactly the proof of optimal substructure property in dynamic programming problems works? They usually say: Let's say the global optimal solution is A, and B is ...
2
votes
2answers
656 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
0
votes
1answer
46 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
518 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
342 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 ...
4
votes
1answer
427 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
1answer
64 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
455 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 ...
-1
votes
1answer
2k 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 ...
0
votes
2answers
913 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
0answers
253 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) $$m^{ed}\...
3
votes
1answer
110 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. ...
1
vote
1answer
2k 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 ...
1
vote
1answer
444 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 ...
5
votes
2answers
533 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 ...
6
votes
0answers
1k 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 ...
1
vote
1answer
307 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
2answers
953 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 ...
23
votes
2answers
2k 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
2k 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 ...
2
votes
2answers
815 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
346 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 ...
1
vote
1answer
774 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
2k 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: <...
5
votes
1answer
4k 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$ ...
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 ...
0
votes
2answers
185 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
392 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 ...
-2
votes
1answer
128 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
124 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 to ...
9
votes
6answers
367 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
0answers
53 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 ...
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. ...