# Questions tagged [correctness-proof]

65 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
103 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 ...
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 ...
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 ...
880 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 ...
46 views

### Longest path length in an undirected tree, can we prove this algorithm is correct (which it is)?

Hello I solved this leetcode https://leetcode.com/problems/tree-diameter/ question reserved for people who pay the subscription. The question: Given an undirected tree (tree is not disjoint), ...
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 ...
349 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 ...
234 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 ...
257 views

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 ...
162 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]. ...
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 ...
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 ...
54 views

### Proof for LeetCode: 11. Container With Most Water problem

UPDATE: I abandoned this initial approach in favor of a more powerful invariant I worked out after posting. I've detailed that one in an answer below. I'm new to algorithm correctness proof-writing ...
67 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 ...
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 ...
49 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: ...
153 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: ...
46 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 ...
89 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 ...
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: ...
78 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 ...
31 views

358 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 ...
256 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: ...
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 ...
11 views

### Verification conditions for Hoare

I am reading about Hoare logic but I don't really understand the verification conditions part for proving partial correctness. What's happening between step 1 to 2? Why do we ignore the Q := 0 and ...
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 <...
18 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: ...
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. ...
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 ...
48 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 ...
54 views

340 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 ...
58 views

### Proof of the average case of the Heap Sort algorithm

Consider the following python implementation of the Heap Sort algorithm: ...
34 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 ...
29 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 ...
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 ...