Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

59 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 ...
6
votes
0answers
997 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 ...
3
votes
0answers
93 views

Are there are satisfying explanations for why genetic algorithms work?

The following commentator writes: Having studied this extensively back when they were called Genetic Algorithms, I would like to offer a few insights. One of the biggest reasons they fell out ...
3
votes
0answers
273 views

Expression of the weakest precondition of a while loop

I am interested in computing weakest preconditions (WP) of loops. If I refer to Wikipedia "Predicate Transformer semantics", the WP for e.g. total correction of a loop annotated with an invariant I ...
3
votes
0answers
757 views

How to prove stability of sorting algorithms?

I know to prove instability, we can simply provide a counter-example. But is there a general way to prove that a sorting algorithm is stable? Could you please tell a general method and then show an ...
3
votes
0answers
225 views

Sequence Alignment with general gap penalties: proof of optimal substructure

I am very well-aware of how optimal substructure for pairwise global sequence alignment using the Needleman-Wunsch algorithm works. However, I have merely seen hand-waving explanations for the ...
3
votes
0answers
251 views

How is Chinese Remainder Theorem used in the proof of correctness for RSA

Question At the very end of (most) proofs of RSA's correctness we have something like $$m^{ed}\equiv m\pmod p$$ $$m^{ed}\equiv m\pmod q$$ Therefore by the Chinese Remainder Theorem (CRT) $$m^{ed}\...
3
votes
0answers
263 views

Maximum Weight Independent Set in Circular-Arc Graphs (Proof of A Lemma)

I am reading the paper: "Maximum Weight Independent Set Of Circular-Arc Graphs and It's Applications" (http://link.springer.com/article/10.1007%2FBF02832044). And I had a question regarding the proof ...
3
votes
1answer
439 views

How to tell if a Heuristic is monotonic

I've applied a Heuristic to a puzzle where I need to move all off the B's the the right of the W's. my Heuristic is the total distance of the B's from the right most W's. my initial state is (B,B,B,*,...
2
votes
0answers
43 views

Interval partitioning problem different approach - arrange lectures in minimum number of classrooms

The problem of scheduling lectures in minimum number of classrooms is as follows: Find minimum number of classrooms to schedule all lecture so that no two occur at the same time in the same room. The ...
2
votes
0answers
72 views

Hoare triple: Loop invariant and partial correctness

Below there is Hoare triple in which variable $a$ is an array of integers, $len$, $x, i$ are integer-valued variables, and $r$ is a Boolean-valued variable. I have to provide a loop invariant (using ...
2
votes
0answers
128 views

Why is it true that given a monotonic heuristic function, A* can be seen as Dijkstra's algorithm where no node needs to be processed more than once?

Maybe I am missing something very easy and obvious. But, I don't understand why estimate cost of source vertex is subtracted from the overall estimate cost, if heuristic function $h$ is monotonic: $$...
2
votes
0answers
36 views

Maximum boundary edges amount of union of rectangles

I've read that the maximum boundary edges amount of union of $n$ rectangles, named $p$, is bounded by $p \leq n^2 + 4n$ I tried to prove this by induction, but it's seems too difficult to me, can ...
2
votes
1answer
192 views

Prove that this solution to the Closest 3-Sum problem always works

I was working on a Leetcode problem, 3Sum Closest. I came up with a solution but struck it down because I didn't think it could be correct. But, turns out it was. I want to know why. Here's the ...
2
votes
0answers
143 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]. ...
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
vote
0answers
95 views

How to prove program solves the problem?

I am preparing for the exam on Theory of Programming class. Now I am trying to solve the task from the sample paper: Task description starts here Given the following problem: A problem is given by ...
1
vote
0answers
43 views

Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
1
vote
1answer
115 views

Proving correctness of the Newton's Method for finding the square root of a number

I'm trying to prove the correctness of this simple square root calculation algorithm using SPARK: ...
1
vote
0answers
45 views

Prove that set of operations form a commutative Monoid

this is my first post on this exchange. I am looking for some help with defining a proof that a set of operations I have designed forms a commutative monoid. (Disclaimer: I am not sure that I have ...
1
vote
0answers
77 views

Prove an algorithm. Give directed graph edge weights such that weight of every cycle is 0

I need to construct a graph with the following properties: $w(u, v)$ = $-w(v, u)$, for every edge $(u, v) \in E$ Weight of all $u \leadsto v$ paths is equal, for every $u, v \in V$ (this is zero ...
1
vote
0answers
22 views

Accounting value of Splay trees?

In Splay trees, by definition - the required element x - rises to the root of the tree, using the operations: zig, zig-zig, zig-zag. And the formula zig of the step is this: ...
1
vote
0answers
65 views

Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...
1
vote
0answers
30 views

Minimize number of comparisons to discover a strict total order

$S$ is a set of $n$ elements with some unknown strict total order. The goal is to discover the greatest $k$ elements, where each step consists of comparing $m\ge 2$ elements at once (so if we compare $...
1
vote
0answers
48 views

Provably correct algorithm/CAS for checking term equalities

Within my research of term rewriting systems (TRS) I stumbled upon a paper (Siekmann, J., and P. Szabó. “The Undecidability of the DA-Unification Problem.” The Journal of Symbolic Logic, vol. 54, no. ...
1
vote
0answers
383 views
1
vote
0answers
68 views

Proving correctness of connected algorithm

Okay, so a graph $G = (V, E)$ is (fully) connected if and only if for every pair of vertices $u, v ∈V,$ $u$ and $v$ are connected in $G$. And that if the vertex set is $V = \{0, 1, . . . , n−1\}$, ...
1
vote
0answers
110 views

Proof of correctness of Bottleneck Dijkstra Algorithm

I am working on a bottleneck multicast tree for which I am using bottleneck Dijkstra algorithm. My question is 1) bottleneck Dijkstra has the same correctness as that of (simple) Dijkstra or not ? ...
1
vote
0answers
757 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
336 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 ...
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: ...
1
vote
0answers
53 views

Conjecture about a matrix column swapping challenge problem

So here is the challenge problem statement: https://icpcarchive.ecs.baylor.edu/index.php?option=com_onlinejudge&Itemid=8&page=show_problem&problem=1512 Basically, given a 0/1 matrix, you ...
1
vote
0answers
2k views

Insertion sort Proof by Induction

I am reading Algorithm design manual by Skiena. It gives proof of Insertion sort by Induction. I am giving the proof described in the below. Consider the correctness of insertion sort, which we ...
0
votes
0answers
45 views

Minimum increment/decrement to change an array into non-decreasing sequence

I was trying to solve a codeforces problem https://codeforces.com/contest/713/problem/C. Basically we have to convert a sequence in minimum increment decrement operations to a non-increasing sequence....
0
votes
0answers
43 views

Making change optimally

Consider that a currency system has $k$ denominations $d_0, d_1, ... d_{k-1}$. $d_0, d_1, ... d_{k-1}$ are such that $d_0 < d_1 < ... < d_{k-1}$ and $d_i$ divides $d_j$ for all $0<=i<j&...
0
votes
0answers
22 views

Using induction vs invariants to prove correctness of algorithms

In my algorithms class I have generally been proving algorithms by induction. So for example, given some algorithm $A(n)$ that computes $x$, I show that the algorithm works for some base case, say $A(...
0
votes
1answer
105 views

how to prove correctness of this BFS algorithm?

Given an undirected connected graph, I wrote the following algorithm based on BFS. The algorithm detects wether this graph contains a cycle. If it contains a cycle then prints it. I'm pretty sure that ...
0
votes
0answers
41 views

Proof of the average case of the Heap Sort algorithm

Consider the following python implementation of the Heap Sort algorithm: ...
0
votes
0answers
31 views

Using Hoare logic to show an invariant holds or using induction?

I want to know if given a while loop: x = 0 while(x < 5){ x = x + 1 } I want to show that x (at the a ith iteration of the loop), the value of i is ...
0
votes
0answers
20 views

Linearithmic solution to finding closest pairs in an array of N elements

I am reading Algorithms 4ed by Sedgewick and Wayne. I came across this algorithm design question that asks the following: Write a program that given an array of N integers, finds a closest pair: two ...
0
votes
0answers
19 views

How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms: {X = |x|} if(x<=0) x:=-x; else skip; {X=x} This is my solution so ...
0
votes
0answers
54 views

Confused with the proof that Edmonds-Karp always monotically increases the shortest-paths

The proof for the lemma from "Introduction to Algorithms by Cormen et. al." is not clear for me. I can't comprehend a few things. Here is a lemma and its proof. My questions are below. The notation ...
0
votes
0answers
69 views

Alternative proof of the fact that heapify can be linear-time

As an exercise, I'm trying to prove by myself that constructing a binary heap from an array in-place can be $O(N)$. I've come up with an idea, but I'm not sure about its correctness. Firstly, I ...
0
votes
1answer
40 views

Finding invariant when detecting a cycle

Let consider a connected graph $G = (V, E)$ which is not oriented. One way to detect a cycle in such a graph is : Create an array : seen of size $\mid V \mid$ with seen[i] = false for all $i$ ...
0
votes
0answers
69 views

Correct invariant of BFS

I am trying to find a correct invariant of BFS. If we represent a queue as $ Q = [a_0;...; a_n]$ such that : $Q.pop() = a_n$ then I found the following invariant which I think is correct (we denote ...
0
votes
1answer
601 views

Prove Recursive formula (Dynamic programming) N(C,i)

I've been asked to prove the correctness of the following recursive formula. The formula is trying to define, how many ways you can spend your money C on the i amount of beers. I did the following ...
0
votes
0answers
118 views

Proof of correctness recursive reverse digit function

This is an attempt to understand better recursion. The following recursive function returns the integer obtained by reversing the digits of an input integer. I'm trying to prove its correctness: <...
0
votes
0answers
48 views

Loop invariant for

The programme returns the number of digits of an integer $n>0$. I still have some difficulties to understand the difference between the loop invariant condition and what the loop should actually ...
0
votes
0answers
138 views

Counting the number of occurences - loop invariant

I'm trying to come up with loop invariant for the following program. k = a[0] m = 1 p = 1 while p < n: if a[p] == k: m += 1 p += 1 return m I ...