Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

63 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
10
votes
0answers
102 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
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 ...
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 ...
4
votes
0answers
849 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
95 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
320 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
1answer
209 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 ...
3
votes
0answers
230 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
255 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
267 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
466 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
59 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
94 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
143 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
37 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
0answers
158 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
50 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 ...
2
votes
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 ...
1
vote
0answers
61 views

Loop invariant of a search algorithm

I have to come up with a proof of correctness of the following algorithm: GuardedSearch(A; v) Input: an array A of n numbers and a number v Output: an index i such that A[i] = v, or NotFound if no ...
1
vote
0answers
97 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
47 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
145 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
82 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
76 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
31 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
51 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
440 views
1
vote
0answers
74 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
113 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
793 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
347 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
247 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 ...
0
votes
0answers
22 views

Is it the right way to find preorder successor in a binary search tree?

I am confused about the case when the given node is a leaf. The code below does seem to work, but if someone asked me to prove the correctness I'd probably fail. Basically, can someone tell me why <...
0
votes
0answers
17 views

How to write the invariants for one version of binary search insertion point (or leftmost entry) algorithm?

If we compare the binary search algorithm (leftmost or insertion point) on Wikipedia: Algorithm 1: ...
0
votes
0answers
16 views

Proving a Hoare Triple does not hold

I have this program specification annotated with a Hoare Triple. Trying to prove that is the case. ...
0
votes
0answers
39 views

Prove grade-school multiplication algorithm applied to binary numbers

I want to prove that the basic multiplication algorithm is correct when applied to binary numbers. I try to follow the steps described here and here but didn't succeed. The basic implementation ...
0
votes
1answer
41 views

Semantic, total and partial correctness

I encountered the following question: Provide a definition of the semantic correctness of algorithm $A$ with respect to pre-condition $\alpha$ and post-condition $\beta$. A well-presented ...
0
votes
0answers
53 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
24 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
275 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
49 views

Proof of the average case of the Heap Sort algorithm

Consider the following python implementation of the Heap Sort algorithm: ...
0
votes
0answers
33 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
27 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
20 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
90 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
51 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
102 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 ...