Re: Can you be a good programmer?

In article <slrnedf5k7.ddq.andrews@xxxxxxxxxxxxxxxx>, Andrew Smallshaw
<andrews@xxxxxxxxxxxxxxxx> writes
On 2006-08-07, mc <look@xxxxxxxxxxxxxxxxxxxxxxxxxx> wrote:

It does not show anything except that you forgot the algebra classes
already :(

He hasn't forgotten anything. He's trying to show that you can get people
to believe a completely illogical "proof."

Yes, and also not to have absolute faith in something because it has
been 'proven'. I recall a book from University dealing with formal
proofs by induction. It gave a computer program to find the largest
value in a list along the lines of:

let a = 0
for each list[i]
if list[i] > a
let a = list[i]
return a

It then gave a formal inductive proof that this program worked. It has
been mathematically proven, so it must be true, right? Well, I checked
the original specification given in the textbook and no. There is no
mention that the list is composed of positive values, so an
entirely negative list is acceptable input. IOW, the bug was
duplicated in both the code and 'proof' because both relied on the
same implicit assumption.


I have some statistics for some IEC61508 projects (it was in an IEE
journal last year) that said the majority of the "bugs" came from the
specifications not the implementation. I think 47 % to 14%

I also believe that Intel on one of their chips fell foul of the same
problem above. The whole lot was done on formal methods but there was a
flaw in the initial specifications. The chip worked to the
specifications but "put negative numbers in" and it did not work.

Does the proof match the spec and is the spec accurate and bomb proof?
--
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills Staffs England /\/\/\/\/
/\/\/ chris@xxxxxxxxxxxx www.phaedsys.org \/\/\
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/



.

Relevant Pages

  • Re: Can you be a good programmer?
    ... It gave a computer program to find the largest ... IOW, the bug was ... specifications but "put negative numbers in" and it did not work. ... Does the proof match the spec and is the spec accurate and bomb proof? ...
    (comp.arch.embedded)
  • Re: Can you be a good programmer?
    ... IOW, the bug was ... specifications but "put negative numbers in" and it did not work. ... Does the proof match the spec and is the spec accurate and bomb proof? ... Wot's the customer go to do wiv it? ...
    (comp.arch.embedded)
  • Re: How to calculate the percentage of each character in a text file?
    ... I was going to say that I noticed a bug in a portion of my code ... whether it would be a bug or not would depend upon the specifications, ... "It is important to remember that when it comes to law, computers ... Only people can be given permission." ...
    (comp.lang.c)
  • Re: OoO L/ST execution in Core/Woodcrest and Power5
    ... the specifications of specific chips. ... Athlon64 "bug" that was caused by speculatively preloading cache lines. ... but a problem when you misdescribed memory maps to the ...
    (comp.arch)