The 2024 Developer Survey results are live! See the results

# Questions tagged [program-correctness]

The tag has no usage guidance.

30 questions
Filter by
Sorted by
Tagged with
188 views

### Would it be possible to run destructors when aborting a thread?

I had a discussion with a C++ developer on whether aborting a thread causes memory leaks. His opinion on how aborting a thread works was all destructors of the stack objects of the thread to abort ...
198 views

### How do I prove correctness of my algorithm that finds a pair of integers in an array that have a sum of 0?

I have designed an algorithm (up to making a pseudocode) that accepts a sorted array as input and finds in $O(n)$ time if there's a pair of elements (integers) in the array that have a sum zero. What ...
• 225
1 vote
55 views

### What is known about the possibility of making a program to validate another program for correctness?

I'm having a question inspired by exercise 14 from section 1.2.1 of Donald Knuth's The Art of Computer Programming. It's phrased in the following way: (R. W. Floyd) Prepare a computer program that ...
• 23
1 vote
235 views

### Prove that the following algorithm for division and remainders of natural numbers is correct

I am currently brand new to the correctness proof method, and have stumbled upon this algorithm which I find very tricky. Prove that the following algorithm for division and remainders of natural ...
1 vote
2k views

### loop invariant of selection sort algorithm

I am asked to write an C code Selection Sort algorithm and use loop invariant to show its correctness. ...
1 vote
114 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 ...
126 views

### Could someone check my recursive program correctness proof that returns $F(x, y) \rightarrow x + y$?

For $k \in \mathbb N$, we define $Q(k)$ as follows: $Q(k):$ let $x, y \in \mathbb N$ and $x$ is a multiple of $3$ and $k = x + y$, then $FUN(x, y)$ terminates and returns $x + y$ I will prove $Q(k)$...
• 203
562 views

### Prove correctness of the iterative algorithm

Description: Given an array nums and a value val, remove all instances of that value in-place and return the new length. Do not allocate extra space for another array, you must do this by modifying ...
• 281
1 vote
396 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 ...
• 45
1 vote
111 views

### What is this operator in "The Temporal Logic of Programs" Pnueli 1977?

In The Temporal Logic of Programs there is an operator first appearing on page 3 (48) under "Partial Correctness" that looks like an elongated super set symbol. What is it?
• 2,553
1 vote
223 views

### What is the loop invariant of the following function?

x = n; y = 0 while x >= b: x = x DIV b y = y + 1 return y This function takes in $n,b\in\mathbb{N}, n > 0, b > 1$, and returns $k\in\mathbb{N}$ ...
• 143
809 views

### Finding the weakest precondition and invariant of while loop

I am trying to find the weakest precondition and invariant of this while loop. I have read and am trying to understand the concept of calculating preconditions based on postconditions. I was wondering ...
• 31
2k views

### Program Correctness, The specification

From Wikipedia: In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. But the problem is that to get ...
1 vote
312 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: ...
• 11
3k views

### Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
• 66
1k views

### Proving correctness of a loop that calculates the sum of array

I am trying to mathematically prove that the following program is correct: ...
230 views

### Does checking for correctness belong predominantly to "semantic analysis"?

Does checking for correctness belong predominantly to "semantic analysis"? Or is it reasonable to be done in earlier phases (in a compiler like construction) as well? Mainly in syntax ...
• 579
412 views

### Why precondition strengtening is sound in Hoare logic

I have problem with understanding why precondition strengthening is sound rule in Hoare logic. The rule is: $${P \implies Q, \{Q\} C \{X\} } \over {\{P\} C \{X\}}$$ I really do not understand why ...
• 162
594 views

### Hoare logic - partial/total correctnes and strength invariant

I'm studying Hoare logic and I can't understand the relation between partial and total correctness regarding loop invariant. Suppose for example that I have the following program: ...
1k views

### Global relabeling heuristic: Push-relabel maxflow

I have a correct, working implementation of the preflow-push-relabel maxflow algorithm [2]. I am trying to implement the global relabeling update heuristic [3], but have run into some issues. I have ...
558 views

### Hoare Calculus Incorrect Assignment Axiom

I'm currently preparing for an exam and recently came across the following exercise and would like to know whether my solution would be correct. Exercise: Prove that the following axiom is not ...
• 113
1k views

### Can we quantify how close a partially correct programs is to being correct?

I know that there is something called partial correctness, but I was wondering if there was a way to tell how close a semi-correct program is to a fully correct program. For example, if you had a ...
• 71
453 views

### Could program verification techniques prevent bugs of the genre of Heartbleed from occurring?

On the matter of the Heartbleed bug, Bruce Schneier wrote in his Crypto-Gram of 15th April: '"Catastrophic" is the right word. On the scale of 1 to 10, this is an 11.' I read several years ago that a ...
31k views

### Formal program verification in practice

As a software engineer, I write a lot of code for industrial products. Relatively complicated stuff with classes, threads, some design efforts, but also some compromises for performance. I do a lot of ...
• 1,642
3k views

### Proof of Program Correctness - Loop Invariants

I've been reading a book on using loop invariants and induction to prove program correctness. Then I came across the following program which got me thinking... Specification for ...
• 181
102 views

### Does this loop invariant guarantee that the variable never changes?

Suppose you have some loop and and integer k: int k = 5; for (int i = 0 ; i < N; i++) { //(*) //do something } The loop invariant at (*) is: $\{ K=k\}$ ...
• 297
1 vote
323 views

### Loop Invariants as Tautologies

Would it be correct to characterize loop invariants as a type of tautology? I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop ...
• 2,931
3k views

### Counting Inversions Using Merge Sort

In Corman, Introduction To Algorithms, 3rd edition, question 2-4 it asks to count the number of inversions in a list of numbers in $\theta( n \lg n )$ time. He uses a modified Merge Sort to ...
• 2,931