The tag has no wiki summary.

learn more… | top users | synonyms

0
votes
2answers
32 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 ...
6
votes
5answers
133 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
198 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 ...
11
votes
2answers
548 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
vote
1answer
759 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 Cube_Root(n) ...
0
votes
1answer
37 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
96 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
1k 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
139 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?
5
votes
3answers
647 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 ...