# Questions tagged [correctness-proof]

273 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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.
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 ...
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 ...
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. ...
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: ...
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 ...
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 ...
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 ...
808 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 ...
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: <...
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 ...
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 ...
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. ...
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 ...
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: ...
767 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-...
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, ...
219 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 ...
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 ...
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 ...
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 ...
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 ...
501 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 ...
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 ...
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 ...
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 ...
508 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 ...
938 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 ...
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 ...
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$ ...
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. ...
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....
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 ...
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 ...
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 ...
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 ...
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 ...
1k views

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

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