Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [program-correctness]

The tag has no usage guidance.

0
votes
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)$...
4
votes
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 ...
1
vote
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 ...
1
vote
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?
1
vote
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}$ ...
2
votes
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 ...
16
votes
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 ...
1
vote
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: ...
4
votes
3answers
1k views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
0
votes
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: ...
-1
votes
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 ...
2
votes
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 ...
0
votes
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: ...
3
votes
1answer
588 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 ...
0
votes
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 ...
7
votes
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 ...
9
votes
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 ...
59
votes
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 ...
2
votes
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 ...
0
votes
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\}$ ...
1
vote
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 ...
3
votes
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 ...
0
votes
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?
7
votes
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 ...