Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
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 ...
3
votes
0answers
228 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 ...
0
votes
1answer
157 views

Loop invariant condition IsPrime program

I'm new to the concept of loop invariant and I'm trying to figure out the loop invariant for a program that returns if an integer is prime and, if not, one possible factorization. My intuition is that ...
4
votes
2answers
1k views

Intuitive proof for Floyd's cycle detection algorithm

I am trying to understand Floyd's cycle detection algorithm. I can see why the algorithm works. When the Hare moves twice as fast as Tortoise, if there is cycle, they will meet definitely at some ...
2
votes
1answer
427 views

Proving correctness of an iterative Fibonacci algorithm

One of the questions in the problem sets that I'm struggling in is this specific number that asks me to prove an iterative Fibonacci algorithm. The algorithm is written below: ...
1
vote
1answer
146 views

Doubt with the halting problem undecidable proof

The Halting problem proof can be seen as the following programs: Ends(P, I) is a program that detects (returns true or false) if the program P will halt or not with the input I Diag( P ): is a ...
0
votes
0answers
139 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 ...
0
votes
0answers
2k views

proof why worst case for bubble sort is array sorted in reverse order

Question 1: Let's say we have bubble sort algorithm which sorts numbers in ascending order. Intuitively one might agree that the worst case input for this algorithm is array already sorted in ...
-2
votes
1answer
62 views

Learning to prove correctness of simple linked-list algorithms

I understand how to use linked lists, and build algorithm using them. But I don't understand how can we prove their correctness, even of simplest algorithm. I haven't even found a good tutorial ...
195
votes
29answers
47k views

Why is writing down mathematical proofs more fault-proof than writing computer code?

I have noticed that I find it far easier to write down mathematical proofs without making any mistakes, than to write down a computer program without bugs. It seems that this is something more ...
1
vote
1answer
166 views

True Postcondition, with true Precondition

In my exam preparation I stumbled across the follwoing exercise regarding pre and postconditions: As far as I understood the question, we need to express some condition for p, such that if that ...
0
votes
0answers
22 views

Does there exist a conservative algorithm to determine if a certain property is satisfied at a certain part of a program?

... x = a / b; For the above code, for example, is there a way to determine whether b could be zero at the time of division, ...
4
votes
1answer
266 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,...
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: ...
2
votes
0answers
86 views

How to write a theorem corresponding to an algorithm's proof of correctness? [closed]

Let $X$ be an algorithm whose correctness supposed to be proved. What is the best practice to write the corresponding theorem? For example: Theorem: Algorithm $X$ correctly computes its output.
0
votes
1answer
85 views

Proof of correctness for a triangulation-algorithm

I'm working on the following exercise: Consider a point set $S = \{ p_1, p_2, ..., p_n \}$ in the plane in general position (i.e., no three points of $S$ are collinear). The points of $S$ have ...
3
votes
0answers
282 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 ...
1
vote
2answers
66 views

Element wise product sum of two arrays

I have two arrays, namely $a$ and $b$. Both have the same length $n$. I have to find the maximum value of $\sum a_i b_j$, in which every element can be used at most one time. My algorithm for solving ...
0
votes
0answers
45 views

Proof problem in Haskell with take and drop

Im learning Haskell and i want to prove take m (drop n xs) = drop n (take (m+n) xs) and drop m (drop n xs) = drop (m+n) xs Somebody can help me please? :)
1
vote
0answers
71 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
103 views

how to prove correctness of this greedy algorithm? [duplicate]

I did exercise problem from Pittsburgh university cs department. homework. Question 8 is somewhat exciting. Q8 is solved using greedy algorithm but I have no idea how to prove. Below is Question. ...
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 $...
5
votes
3answers
1k views

How to select a binary tree node uniformly at random

The exercise I'm trying to solve is You are implementing a binary search tree class from scratch, which, in addition, to insert, find and delete, has a method ...
1
vote
1answer
332 views

Algorithm for finding 2 missing items in a stream of integers

I saw this post and wondered why the approach described in the accepted answer works. The same problem and solution is described a bit nicer here. So let's say we receive a stream of $n-2$ pairwise ...
0
votes
1answer
60 views

Proof of correctness of this algorithm

Assume $A$ is an array that contains sorted integers , ie $\forall\ i,j$ where $1 \le i \le j \le |A|$, $A_i \le A_j$. The numbers do not have to be unique, and the task is to check if there is at ...
1
vote
0answers
49 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. ...
3
votes
0answers
766 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 ...
1
vote
1answer
84 views

Proving by induction that a function gets called n-1 times

This is the pseudo-code from the problem: ...
2
votes
0answers
29 views

Why can optimality be preserved when inserting a new conjunct into an optimally ordered conjunction of conditions? [duplicate]

In a programming language with short-circuiting, a conjunction of N independent conditions has the following expected cost: where: ...
4
votes
1answer
1k views

Greedy algorithms: Minimum sum number pairing

Given $n$ real numbers (where $n$ is even) find a pairing which minimizes the maximum sum of a pair. I think the optimal pairing is obtained by sorting the original set, pairing the first element ...
1
vote
1answer
47 views

Proof that locality is sufficient in showing two graphs are isomorphic

Using the graph representation with (node, [list of neighbours]), to show that two graphs are isomorphic it is sufficient to: show that the vertices have the same degree and for every pair of ...
1
vote
3answers
324 views

Prove correctness for computing the nth Fibonacci number for the pseudo code

How do we prove the correctness of this pseudo code by induction? ...
1
vote
2answers
311 views

Prove correctness of iterative LCM algorithm

I have been trying to prove the following algorithm, without success. Here is the C-Style pseudocode: ...
1
vote
1answer
326 views

How do we know INVERSIONS-COUNT algorithm implemented in balanced tree really works?

How do we know INVERSIONS-COUNT algorithm (exercise 14.1-7 from here), implemented in balanced tree really works? We assume that the tree data structure we're using is an order statistic tree which ...
0
votes
1answer
117 views

How to prove the outcome of both segment of code are equal

Is it possible to prove using induction? If possible what would be the steps to proof A=B? Main thing i want to proof is outcome of two segments of code are same. Below is the code: Segment A: <...
2
votes
1answer
2k views

Correctness of algorithm to find maximum in array

I want to show correctness of "Algorithm to find maximum element in array" using induction and contradiction. ...
2
votes
0answers
100 views

Missing assumptions in selection algorithm proof of correctness by contradiction? [duplicate]

Yes, this is homework. I need help knowing how to begin this problem: Let A be an algorithm that finds the kth largest of n elements by a sequence of comparisons. Prove by contradiction that A ...
-1
votes
1answer
495 views

Why do we need optimal substructure for dynamic programming?

Cormen and others in their book on algorithms in chapter "15 Dynamic Programming" repeat again and again that we need to prove that "a problem exhibits optimal substructure". A problem exhibits ...
1
vote
1answer
204 views

Shunting-yard algorithm - proof

How can one prove that a shunting-yard algorithm always returns a correct expression in RPN? I cannot find any proof in the internet.
1
vote
2answers
180 views

Can algorithm discovery be brute forced?

Ultimately, when you compile them to machine code, algorithms are just 1's and 0's. So then - could you brute force the genesis, and thus the discovery of new, useful algorithms? Say, in pursuit of ...
1
vote
4answers
151 views

How to prove that algorithm returns the value which appears more than $n/2$ times in the array?

Given the following algorithm (pseudocode): ...
1
vote
0answers
69 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\}$, ...
7
votes
1answer
4k views

Complete examples of program correctness proofs

Does anyone have any complete example of a proof of program correctness? I'm talking about something that includes the usual predicate, base case, inductive hypothesis, and inductive step. But also ...
3
votes
1answer
444 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,*,...
3
votes
1answer
212 views

Proof of Randomized Self-Adjusting Binary Search Tree

I developed a randomized self-adjusting binary search tree years ago, which I called a shuffle tree, but was unable to ever have it published because my proofs were rejected (with little explanation). ...
2
votes
1answer
88 views

Little-O: $\forall c \in \mathbb{R^+}, \exists n_0 \in \mathbb{R^+}, \forall n \in \mathbb{N}, n ≥ n_0 ⇒ g(n) \leq cf(n)$

So I'm assuming everyone's familiar with the definition of Big-O: \begin{align} ∃c \in \mathbb{R^+}, \exists n_0 \in \mathbb{R^+}, \forall n \in N, n \geq n_0 ⇒ g(n) ≤ cf(n) \end{align} Here is ...
1
vote
3answers
2k views

Proof of linear search?

Consider the searching problem: Input: A sequence of $n$ numbers $A=(a_1, a_2, \ldots , a_n)$ and a value $v$. Output: An index $i$ such that $v = a_i$ or the special value NIL if $v$ does not ...
0
votes
1answer
1k views

Divide and Conquer majority element algorithm

The algorithm should return the majority element if it exists (majority meaning that there are $> n/2$ occurrences in the array) I came up with this linear divide and conquer algorithm, but I'm ...
1
vote
0answers
111 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 ? ...