# Questions tagged [program-correctness]

The tag has no usage guidance.

24 questions
2answers
72 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)$...
1answer
94 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 ...
1answer
107 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 ...
1answer
95 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?
1answer
101 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}$ ...
0answers
663 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 ...
2answers
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 ...
0answers
209 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: ...
3answers
1k views

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

Consider the following algorithm for computing integer powers: ...
1answer
693 views

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

I am trying to mathematically prove that the following program is correct: ...
1answer
98 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 analysis. Or is ...
1answer
306 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 ...
1answer
422 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: ...
1answer
588 views

### Global relabeling heuristic: Push-relabel maxflow

I have a correct, working implementation of the preflow-push-relabel maxflow algorithm . I am trying to implement the global relabeling update heuristic , but have run into some issues. I have ...
2answers
338 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 ...
5answers
456 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 ...
6answers
360 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 ...
5answers
17k 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 ...
1answer
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 ...
1answer
66 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\}$ ...
3answers
175 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 ...
1answer
2k 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 ...
1answer
302 views

### Can GDB debug itself?

Can GDB be run on itself? How or why not? I see something about it http://www.math.utah.edu/docs/info/gdbint_3.html But GDB might not be written in a language that it can debug?
6answers
3k views

### Can all languages have semantic and logical errors?

I have been reading about PHP and many authors mention semantic and logical errors separately. As an example of a semantic error, they give a function called with incorrect number of parameters: this ...