Questions tagged [program-correctness]
The program-correctness tag has no usage guidance.
31 questions
0
votes
0
answers
18
views
Row Echelon Form - Java Code Correctness
I wrote some code that calculates the REF (Row Echelon Form) of a matrix in Java, and I was wondering if my final code is implementing the correct algorithm to solve for it (the code is similar to the ...
2
votes
2
answers
278
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 ...
- 261
0
votes
1
answer
273
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
0
answers
57
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
1
answer
251
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 ...
- 11
1
vote
0
answers
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.
...
user127304
1
vote
0
answers
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 ...
- 69
0
votes
2
answers
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
4
votes
1
answer
583
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
1
answer
417
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
1
answer
113
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
1
answer
225
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
2
votes
0
answers
818
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
20
votes
2
answers
3k
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 ...
- 365
1
vote
0
answers
313
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
4
votes
3
answers
3k
views
Finding a good loop invariant for a powering procedure
Consider the following algorithm for computing integer powers:
...
- 66
0
votes
1
answer
2k
views
Proving correctness of a loop that calculates the sum of array
I am trying to mathematically prove that the following program is correct:
...
- 125
-1
votes
1
answer
237
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
3
votes
1
answer
416
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
0
votes
1
answer
601
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:
...
- 155
3
votes
1
answer
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 ...
user26203
0
votes
2
answers
564
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
7
votes
5
answers
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
9
votes
6
answers
455
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 ...
- 535
91
votes
8
answers
32k
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,692
2
votes
1
answer
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
0
votes
1
answer
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
3
answers
328
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,941
4
votes
1
answer
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,941
0
votes
1
answer
612
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?
- 1,016
7
votes
6
answers
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 ...
user970696