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]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
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 ...
2
votes
1answer
3k views

Correctness proof: 2-approximation of greedy matching-algorithm

Input: number of edges and vertices, and array of all edges in graph. Output: array of edges that construct a matching, so that: $$\frac{\text{the number of edges in this matching}}{\text{the number ...
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{\...
2
votes
0answers
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 ...
-1
votes
1answer
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)$: ...
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 ...
4
votes
1answer
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 ...
-2
votes
1answer
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 ...
0
votes
0answers
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. ...
5
votes
2answers
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 ...
0
votes
2answers
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: ...
3
votes
2answers
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 ...
0
votes
0answers
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 ...
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 ...
2
votes
1answer
441 views

Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps ...
1
vote
2answers
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 ...
3
votes
1answer
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 ...
1
vote
0answers
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: ...
2
votes
1answer
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 ...
3
votes
1answer
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 ...
4
votes
3answers
1k views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
3
votes
1answer
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 ...
2
votes
1answer
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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$ ...
0
votes
1answer
356 views

Longest double increasing subsequence (LIS variant)

I'll start with the definitions:Let $S = s_1s_2...s_n$ be a sequence of $n$ integers. A double increasing subsequence of $S$ is a sequence $P=p_1p_2...p_k$ (not necessarily continuous) where for each $...
2
votes
2answers
19 views

Can I use the set of “used arguments values” as a memoization key for a deterministic function?

I have a deterministic function $f(x_1, x_2, ..., x_n)$ that takes $n$ arguments. Given a set of arguments $X = (x_i)$, I can compute $U_X = \{ i \in [1, n] : x_i \text{ was read during the ...
2
votes
1answer
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 ...
1
vote
2answers
137 views

Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
3
votes
1answer
752 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[...
1
vote
2answers
291 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
1answer
913 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: ...
1
vote
5answers
496 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
2answers
1k views

Trouble finding loop invariant for this while loop

I'm having trouble coming up with an invariant for proving partial correctness of this function. ...
4
votes
1answer
261 views

Proof Carrying LLVM?

I am intrigued by and understand the very basics of Proof Carrying Code (PCC) and I recognize that LLVM is a machine-independent intermediate language. LLVM is the intermediate form of many languages,...
2
votes
1answer
371 views

CLRS Rod Cutting Inductive proof

I'd like to preface this question by saying that it is not a homework question. However, it is a question regarding the course material. In the rod-cutting example an equation is presented to ...
6
votes
2answers
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-...
-2
votes
1answer
202 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
792 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
252 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 ...
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 ...
1
vote
2answers
209 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)$ ...
0
votes
1answer
104 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 ...
2
votes
2answers
643 views

Understanding Log(n) Loop Invariant

When attempting to find the following loop invariant for: ...
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{...
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
510 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 ...