The tag has no usage guidance.

learn more… | top users | synonyms

1
vote
0answers
31 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
206 views

Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers: ...
-1
votes
1answer
47 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
32 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
49 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
102 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
143 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
137 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
205 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 ...
8
votes
6answers
272 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 ...
25
votes
5answers
3k 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
2k 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
50 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
115 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
209 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?
6
votes
6answers
2k 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 ...