We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
194
votes
29answers
47k views

Why is writing down mathematical proofs more fault-proof than writing computer code?

I have noticed that I find it far easier to write down mathematical proofs without making any mistakes, than to write down a computer program without bugs. It seems that this is something more ...
110
votes
14answers
13k 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 ...
29
votes
2answers
26k views

How to prove greedy algorithm is correct

I have a greedy algorithm that I suspect might be correct, but I'm not sure. How do I check whether it is correct? What are the techniques to use for proving a greedy algorithm correct? Are there ...
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 ...
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.
19
votes
5answers
5k views

Example of an algorithm that lacks a proof of correctness

We have Hoare logic. Why is it still possible that an algorithm is right but there is no proof that it's correct? Suppose the algorithm is expressed in C. Then we can argue step by step that it's ...
10
votes
3answers
7k views

Trying to understand this Quicksort Correctness proof

This proof is a proof by induction, and goes as follows: P(n) is the assertion that "Quicksort correctly sorts every input array of length n." Base case: every input array of length 1 is already ...
10
votes
2answers
970 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. ...
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: ...
9
votes
6answers
366 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 ...
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 ...
9
votes
0answers
99 views

Can we say McCarthy and Hoare had the same objective in the 60s regarding a mathematical theory of computation?

I don't think there's any way to ask a very precise question here, so this might be considered opinion based. Nevertheless, it seems the question is clear enough because I'm asking whether these two ...
7
votes
2answers
807 views

Proof of correctness of algorithm to determine whether the elements of an array are repeated an equal number of times

I apologize for the long title, but I really didn't know how to write it different without lacking informations about the content. I recently had an university exam about Parallel Algorithms. One ...
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: <...
7
votes
1answer
4k 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 ...
7
votes
2answers
5k 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$ of ...
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. ...
6
votes
1answer
3k views

Why proving programs correctness doesn't have the same importance as algorithms analysis or the theory of computation in practice?

What are the major causes that makes "Proving Programs correct", not a widely attractive subject? though from it's name, and from what we know from other disciplines (like mathematics) it looks like ...
6
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: ...
6
votes
2answers
764 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-...
6
votes
1answer
440 views

Theory of multi-label classification

Multi-label classification is a machine-learning problem where each sample can have zero or more labels from a closed set of possible labels. This task has applications in several fields. For example, ...
6
votes
1answer
218 views

Proof: “If the list is then k-sorted for some smaller integer k, then the list remains h-sorted”

Shellsort is a generalization of insertion sort that allows the exchange of items that are far apart. The idea is to arrange the list of elements so that, starting anywhere, considering every hth ...
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 ...
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 ...
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 ...
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 ...
5
votes
2answers
498 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 ...
5
votes
3answers
1k views

How to select a binary tree node uniformly at random

The exercise I'm trying to solve is You are implementing a binary search tree class from scratch, which, in addition, to insert, find and delete, has a method ...
5
votes
2answers
134 views

Must the champion of an entire tournament beat the champion of a possible tournament among other players?

I have a list of "players" of a "tournament". Any two adjacent players may "compete", which results in the loser being thrown out of the tournament. Winning is not transitive. The winner of a given ...
5
votes
2answers
309 views

Curious about an old algorithm which calculates modular inverse

I am not sure if I should ask this question here or somewhere else. In fact, I initially asked my question here at mathoverflow.net but it was marked as off-topic Background: I was searching through ...
5
votes
2answers
506 views

Is the inverse of MST cycle property always true? Why?

I am trying to find an algorithm which would check for each edge in a given weighted undirected graph whether it belongs to any of the graph's Minimum Spanning Trees. I have found many potential ...
5
votes
2answers
935 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 ...
5
votes
2answers
1k views

Find all critical edges for minimum spanning tree

This is a problem from the textbook "Algorithms, 4th edition" by Robert Sedgewick and Kevin Wayne. 4.3.26 Critical edges. An MST edge whose deletion from the graph would cause the MST weight to ...
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$ ...
5
votes
1answer
923 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
383 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....
5
votes
1answer
930 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
2answers
2k views

What does it mean to “strengthen the precondition and weaken the postcondition” in Hoare logic?

Having learned a rough summary of Hoare logic (i.e. learning just the basic concept of Hoare triples and a few of the rules) I kept seeing a statement along these lines: The rule of consquence ...
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 ...
4
votes
2answers
13k views

Prove correctness of recursive Fibonacci algorithm, using proof by induction

I'm studying for the computer science GRE, and as an exercise I need to provide a recursive algorithm to compute Fibonacci numbers and show its correctness by mathematical induction. Here is my ...
4
votes
2answers
619 views

Prove that the total distance is minimised (when travelling across the longest path)

Here is the problem: Given a tree $T$, I need to visit every node in the tree once. I can start and end anywhere I want. I would like to travel the least distance possible when doing so. I don't have ...
4
votes
3answers
1k views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
4
votes
2answers
177 views

Is asymptotic ordering preserved when taking log of both functions?

In one of my exercise sheets I have the following question; Let $f,g\colon \mathbb{N}\longrightarrow\mathbb{R}$ be positive functions with $f(n) \in O(g(n))$. Prove or disprove; $\ln(f(n)) \in O(\ln(...
4
votes
1answer
1k views

Greedy algorithms: Minimum sum number pairing

Given $n$ real numbers (where $n$ is even) find a pairing which minimizes the maximum sum of a pair. I think the optimal pairing is obtained by sorting the original set, pairing the first element ...
4
votes
2answers
113 views

Is structural induction on terms applicable when a function is involved?

Assume an evaluation-relation on terms $t \Downarrow v$. If I want to prove correctness of a function $\phi$ w.r.t. evaluation, I have to show that the following implication always holds: $$\frac{\...
4
votes
1answer
821 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 ...
4
votes
1answer
124 views

Mistake in a proof of termination phase of Simplex algorithm in CLRS?

There is a pseudo-code for Simplex algorithm in CLRS: The proof consists from three-part loop invariant: Proof We use the following three-part loop invariant: At the start of each iteration ...
4
votes
2answers
1k views

Intuitive proof for Floyd's cycle detection algorithm

I am trying to understand Floyd's cycle detection algorithm. I can see why the algorithm works. When the Hare moves twice as fast as Tortoise, if there is cycle, they will meet definitely at some ...
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 ...
4
votes
1answer
531 views

Help Finding Loop Invariant From For Loop

I have created the algorithm below... ...