Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.

# Questions tagged [correctness-proof]

273 questions
Filter by
Sorted by
Tagged with
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 ...
3k views

49 views

### Structural induction in non-local program transformation

Assume a functional language and a specialization operation (pulling out sub-expressions): let f x y = (h 23 x) + (g 42 y) becomes ...
759 views

### Proof of correctness of divide and conquer clique algorithm

I have the following divide and conquer algorithm that finds a clique in an undirected graph $G = (V, E)$: ...
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 ...
79 views

### How would P2P Kriegspiel be designed?

Kriegspiel chess is a variant of chess in which each player is not aware of where the opponent's pieces are. In a human match, a trusted intermediary relays piece losses, legality of moves etc. This ...
214 views

### Proof Knuth S algortihm correctness

In the programming pearls book by Jon Bentley, there is a section about the problem of finding a random set of m integers from range 0 to n-1 integers. To do so they use Knuth's algorithm given by the ...
208 views

### How does the induction proof work in this example?

Refer to answer 1.1 of this file: http://www.dei.unipd.it/~geppo/AA/DOCS/NPC.pdf From my understanding and this thread, https://math.stackexchange.com/a/928412, we need 3 steps for that proof. ...
509 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 ...
599 views

### Algorithm for length of longest common subsequence

The case of multiple strings. A slight modification of the dynamic programming algorithm for two strings is used as a subroutine. Here is the pseudo code: ...
888 views

### Is bounded waiting ensured in given version of Dekker's solution for critical section problem?

William Stallings discuss various step by step process in developing Dekker's algorithm in his Operating Systems book. In process, he reaches to following version of algorithm (which is incomplete as ...
169 views

### Greedy algorithm correctness proof (UVA 10716)

Given an input string, not necessarily a palindrome, compute the number of swaps necessary to transform the string into a palindrome. By swap we mean reversing the order of two adjacent symbols (UVA ...
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 ...
441 views

### Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps ...
568 views

### What is the point of the “respect” requirement in cut property of minimum spanning tree?

The cut property stated in terms of Theorem 23.1 in Section 23.1 of CLRS (2nd edition) is as follows. Theorem 23.1 Let $G = (V, E)$ be a connected, undirected graph with a real-valued weight ...
2k views

### Proof of 0/1 knapsack optimal substructure

I'm trying to understand why exactly the 0/1 knapsack problem actually has the optimal substructure property. Let $E$ be the set of items to consider and $v$ and $w$ the value and weight functions ...
231 views

### I need help understanding how to prove partial correctness

Please help me understand how I would prove the partial correctness of the below pseudocode with respect to the following predicates: Pre: {n>=0} Post: ...
195 views

### How to use the concept of loop invariant to reduce errors in loops?

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Here is an small example ...
865 views

### How to find loop invariant from weakest precondition?

Consider this code: Precondition: Postcondition: rv == i <==> ∃i, 0 ≤ i ≤ a.length-1, a[i] == key ...
1k views

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

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

### Modal logic axiom S4, transitive and reflexive frame, tableaux solver

I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4. So, here is some background knowledge that can be useful: S4 axiom is a class of transitive and ...
3k views

### Proof of correctness of A star search algorithm

I've been looking for the proof of correctness for the A star (A*) algorithm but none of the texts and websites offer it. Mostly they are talking about the proof of optimality of the A* algorithm. I'm ...
145 views

### Validate that a threaded binary tree works as intended

I am attempting to validate that my threaded binary tree’s insertion and deletion works as intended. Would it be safe to assume that the following procedure would have tested all corner cases at ...
4k views

### Proof by Reduction: From Empty Language to Halting Problem on Empty Input

Question: Let language $E$ = {$\langle M \rangle$ | $M$ accepts no inputs whatsoever} Let language $H$ = { $\langle M \rangle$ | $M$ halts on an empty string input}. Is it possible to show that $H$ ...
356 views

129 views

### Quicksort $T(n)_{best}=\Omega(n\log n)$ proof

About the proof that quicksort has $T(n)_{best}=\Omega(n\log n)$. I can't find this specific aspect anywhere online which is strange. I'm going through a proof for this in a book and I don't ...
137 views

### Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
752 views

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 ...