Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
7
votes
2answers
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 ...
18
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 ...
2
votes
2answers
289 views

How can I prove that a cryptography algorithm is a pseudo-random number generator?

I have read about cryptography prgs. If I have a generator G(x1,x2...,xn)= x1,x2,...,xn, x1&x2...&xn , how can I prove that it is a prg or prove it is not? Is there some principles I have ...
0
votes
1answer
448 views

find if a string is periodic using a suffix tree, and prove it

A string s of length n is periodic if there is a string $u$ of length <= n/2 such that $s = u^ku'$, where $k$ is ...
2
votes
0answers
150 views

Correctness proof of the algoritm to generate permutations in lexicographic order

The following algorithm generates the next permutation lexicographically after a given permutation. It changes the given permutation in-place. Find the largest index k such that a[k] < a[k + 1]. ...
0
votes
1answer
106 views

What does the algorithm calculate?

We have the following ...
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 ...
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 ...
0
votes
2answers
864 views

What are the flaws in this encryption algorithm?

Let $A$ be a randomly generated matrix. Let $I$ be the identity matrix. $\times$ is the matrix multiplication operation, $/$ is matrix division (multiplying the first matrix by the inverse of the ...
5
votes
2answers
310 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 ...
1
vote
0answers
770 views

Correctness of Dijkstra's algorithm

This question is about the correctness proof of Dijkstra's algorithm in the third edition of Introduction to Algorithms by Cormen et al. (pages 660–661). The proof makes a case that considering path $...
1
vote
0answers
337 views

Proof that the length of the largest ascending subsequence is the number of decreasing subsequences

Given a sequence of numbers, I have to prove that the number of decreasing subsequences (non-strictly), so that every number is included in one subsequence and the number of subsequences is minimum is ...
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 ...
0
votes
1answer
177 views

Cards shuffling. Greedy algorithm

We have n deck of cards. To shuffle i-th deck we need a(i) seconds. Our task is to give a greedy algorithm, which will merge two decks until we have one deck. My idea is to create a priority queue. ...
0
votes
0answers
76 views

Boys And Girls Problem. How to prove that the algorithm is correct?

Given that, there are 10 children standing in a circle, 8 of them stand next to a boy, and 4 of them stand next to a girl. If 7 boys and 3 girls stand in the following order: GBGBGBBBBB, then 8 ...
2
votes
1answer
176 views

Graph splitting via an algorithm and proof of properties

Given the following function: ...
1
vote
1answer
60 views

Generate collision resistant identifiers with two-way hashing

Objective: We want to generate a unique and reproducible identifier for a given slice of bytes and avoid collisions. High-level idea: Compute $$fK := hash(k_1)\; and\; sK := hash(k_1^{-1})\; where\; ...
1
vote
3answers
4k views

Correctness proof of greedy algorithm for 0-1 knapsack problem

We have a 0-1 knapsack in which the increasing order of items by weight is the same as the decreasing order of items by value. Design a greedy algorithm and prove that the greedy choice guarantees an ...
4
votes
2answers
115 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{\...
0
votes
1answer
360 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 $...
3
votes
1answer
351 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
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
766 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 ...
0
votes
2answers
601 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: ...
2
votes
1answer
386 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 ...
0
votes
0answers
209 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. ...
3
votes
2answers
906 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 ...
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 ...
0
votes
0answers
175 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 ...
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 ...
2
votes
1answer
458 views

Proving correctness of an exponentiation routine

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

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
2
votes
1answer
265 views

Invariant Proof of For Loops?

From CLRS (third edition, page 19), there is a footnote: When the loop is a for loop, the moment at which we check the loop invariant just prior to the first iteration is immediately after the ...
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. ...
3
votes
1answer
881 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 ...
1
vote
1answer
147 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$ ...
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
139 views

Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
3
votes
1answer
755 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
299 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
499 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 ...