Questions tagged [correctness-proof]

Questions that ask for or about correctness proofs of algorithms.

Filter by
Sorted by
Tagged with
0
votes
0answers
12 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
31 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
30 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
1answer
54 views

Reduction from Vertex Cover to Dominating Set

I am trying to reduce the vertex cover (decision) problem to the dominating set (decision) problem in order to prove that the latter is NP-hard. After some research online, I found that many articles ...
-1
votes
0answers
13 views

Recursive definition character counter

This is my definition for part 1 (in latex form) \begin{alignat*}{2} \text{Base Case }& &&\text{ if } \mathtt{ones}(\varepsilon) = 0 \qquad \mbox{ ($\varepsilon$ is the empty ...
0
votes
1answer
24 views

I cannot find an invariant for the following program

I have the following: (|$y=0; x=c$|) while(x > 0){y=y+a; x=x-1;} (|$y= a*c$|) This seems like a fairly simple program and I can intuitively tell that the post ...
2
votes
1answer
25 views

Proving inequalities related to Dijkstra's algorithm

Define $spdist(s,t)$ as the distance of the shortest path from vertex $s$ to $t$. Define $IN(v)$ as the set of in-neighbors of $v$. Define $w(u,v)$ as the weight of the edge $(u,v)$. I am asked to ...
4
votes
2answers
194 views

Is asymptotic ordering preserved when taking log of both functions?

In one of my exercise sheets I have the following question; Let $f,g\colon \mathbb{N}\longrightarrow\mathbb{R}$ be positive functions with $f(n) \in O(g(n))$. Prove or disprove; $\ln(f(n)) \in O(\ln(...
0
votes
0answers
45 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&...
2
votes
0answers
45 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 ...
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 ...
0
votes
0answers
23 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
149 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
1answer
19 views

Loop invariant initialisation confusion

Consider the algorithm LastMatch below, which returns the offset (shift) of the last occurrence of the pattern P in text T, or -1 if P does not occur in T: ...
0
votes
0answers
42 views

Proof of the average case of the Heap Sort algorithm

Consider the following python implementation of the Heap Sort algorithm: ...
1
vote
1answer
54 views

Minimize cost of recursive pairwise sums: how to prove the greedy solution works?

The problem is in this other question. Why does this always work? It's not clear to me how one would use induction. For $n = 3$, a quick calculation shows it works, however, I don't think it ...
0
votes
0answers
32 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 ...
1
vote
0answers
33 views

Where to get proofs of open problems checked? [closed]

I have found what I believe is a proof of related to an open problem in computer science. I've written it up in LaTeX, and I am looking for a way to get it evaluated. I know that cs.se/cstheory.se ...
0
votes
0answers
21 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
1answer
72 views

Confusion about assignment axiom in Hoare logic

I wanted to know if we are given the f.f.g. Hoare triple: {x = 43}x := x + 1{x = 44} How do we show that this is a valid Hoare triple? My attempt was: Using the assignment axiom: {x + 1 = 43} x := ...
3
votes
1answer
109 views

Prove that the greedy algorithm to remove k digits from a n-digit positive integer is optimal

Given a positive n-digit integer, such as 1214532 (n=7), remove k digits (for example k=4) such that the resulting integer is the smallest one. A greedy algorithm for this would keep removing digits ...
1
vote
1answer
62 views

In-place matrix transposition using rotations

Some time ago I invented an algorithm for in-place matrix transposition using rotations. A matrix of size N×M is represented as a one-dimensional array of size N*M, which is also the future storage ...
1
vote
1answer
28 views

Dubins TSP NP-hardness proof detail

In Le Ny et al.'s paper On the Dubins Traveling Salesman Problem (https://tinyurl.com/y59f7d8x) the authors prove, among other works, that the Dubins Traveling Salesman Problem (DTSP) is NP-hard. I ...
3
votes
3answers
58 views

Why is subarray $A[p..k-1]$ empty when $k=p$?

I'm working through a proof of correctness for merge sort. I'm given a loop invariant for a for loop, which makes reference to a subarray $A[p..k-1]$. During the initialization step of the ...
4
votes
1answer
124 views

Mistake in a proof of termination phase of Simplex algorithm in CLRS?

There is a pseudo-code for Simplex algorithm in CLRS: The proof consists from three-part loop invariant: Proof We use the following three-part loop invariant: At the start of each iteration ...
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 ...
2
votes
1answer
127 views

Understanding Correctness of Bidirectional Dijkstra

I'm trying to understand the correctness of the bidirectional version of Dijkstras algorithm as mentioned here on slide 10: https://www.cs.princeton.edu/courses/archive/spr06/cos423/Handouts/EPP%...
1
vote
1answer
63 views

Do the minimum spanning trees of a graph have the same number of edges with a given weight?

I'm asking about the answer here: Do the minimum spanning trees of a weighted graph have the same number of edges with a given weight? I didn't understand the best answer here Choose edge $e \in ...
0
votes
1answer
73 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
72 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
42 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$ ...
2
votes
0answers
85 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 ...
3
votes
2answers
3k views

Why is this a proof by contradiction for this algorithm? Isn't this a direct proof instead?

First Slide: Find Max(A) // INPUT: A[1..n] - an array of integers // OUTPUT: an element m of A such that m >= A[j], for all 1 <= j <= A.length max = A[j==1] for j = 2 to A.length if max < A[...
1
vote
0answers
46 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
117 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: ...
4
votes
2answers
620 views

Prove that the total distance is minimised (when travelling across the longest path)

Here is the problem: Given a tree $T$, I need to visit every node in the tree once. I can start and end anywhere I want. I would like to travel the least distance possible when doing so. I don't have ...
2
votes
0answers
84 views

Comparing locally maximal and localy minimal Hamiltonian paths [closed]

Let $K_n$ be a weighted complete graph on $n$ vertices. Two Hamiltonian paths are formed as follows. The first one, $H$, is formed by starting at an arbitrary vertex, and at each stage proceeding from ...
0
votes
0answers
80 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 ...
2
votes
1answer
37 views

Correctness of an algorithm difference between recursive and iteraive

I know that the general strategy to do the correction of an algorithm is as follow : if the algorithm is recursive then prove the correctness using induction if the algorithm is iterative (...
0
votes
1answer
60 views

Find an invariant in the minimum algorithm

I have the following simple algorithm to find the smallest element of an array $A$ of numbers: ...
5
votes
2answers
135 views

Must the champion of an entire tournament beat the champion of a possible tournament among other players?

I have a list of "players" of a "tournament". Any two adjacent players may "compete", which results in the loser being thrown out of the tournament. Winning is not transitive. The winner of a given ...
0
votes
1answer
536 views

Is my proof of my greedy algorithm to find subsequence correct?

Credit to KleinBerg and Taros Book Some of your friends have gotten into the burgeoning field of time-series data mining, in which one looks for patterns in sequences of events that occur over time. ...
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
281 views

Proof that G is a Tree After DFS and BFS form the same tree T [closed]

Let G be a connected, undirected graph containing some vertex s. let's say that BFS and DFS are both run on G starting at s and that the breadth first search and depth first search ...
0
votes
2answers
65 views

Prove that the following algorithm has STOP property (number of steps is finite)

Prove that the following algorithm has STOP property. I am not sure if this term is widely know, so the definition of STOP property that I got during classes looks as follows: STOP property (for ...
2
votes
2answers
280 views

Iterative Fibonacci algorithm correctness proof, finding loop invariants

The algorithm take in an integer $n$ and outputs the $n$th number in the Fibonacci sequence ($F_n$). The sequence starts with $F_0$. I am trying to prove the correctness assuming valid input: ...
2
votes
0answers
131 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: $$...
1
vote
2answers
326 views

Proof of QuickSort algorithm correctness

Recently I’ve studied QuickSort and understood its general idea. Basically, we do the following: Pick an element from the array (no matter which one and how in this context) Rearrange elements in ...
2
votes
1answer
432 views

Confused about the correctness proof of Dijkstra's algorithm

In the proof of the correctness of Dijkstra algorithm, there is a lemma stating as follow: Let u be v's predecessor on a shortest path P:s->...->u->v from s to v. Then, If d(u) = δ(s,u) and edge (...
0
votes
1answer
397 views

How this proof of fractional knapsack works?

I don't understand a step in my book proving the fractional knapsack problem: Let value of items $v_1\ge v_2\ge \dots\ge v_n$, and assume $X=\langle x_1, \dots,x_n\rangle$ are the solution by ...