h2g2 The Hitchhiker's Guide to the Galaxy: Earth Edition

http://www.h2g2.com/A514379

What it means for a computer program to be correct
How you can prove that a program is correct.

I'm particularly proud of the non-technical example... [winkeye]

Comments, criticisms, typos, nitpicks, all very much welcome.

I posted a comment inadvertantly on the other thread, here's the text:

"Interesting article.

The example you gave of a partially correct program might need revision.

The program would either buy a winning ticket and be finished, or keep buying new tickets until you are totally broke. Instead of leading from [i am poor] to [i am rich] it leads to [i am broke]and will stop because there is no more money left to buy lottery tickets for.
What you were looking for is a program that would keep going ad infinitum until it could end."

~^M^~

nod - hopefully that thread will get sinbinned shortly...

If I added "Earn a pound busking" to it, that would work, wouldn't it?

Great entry; it really made me think.

A few typos here and there; the ones I remember were 'garauntee' in the 'Asking the Question' section, which should be 'guarantee', and 'corectness' and 'if' (which should read 'is' in the result of the rules of inference) in the 'rules of inference' bit.

The bit on the Floyd-Hoare logic or whatever is relatively unclear to the layperson (ie me ), but it did remind me a hell of a lot of coding my own extremely rudimentary text adventures as a 13 year old using Amiga Basic, when the inference conditions needed to present the player with a variety of choices at an input stage read something like this:
10 PRINT "The path splits into three. Which way do you want to go - North, North-west or North-east?"
20 INPUT A$
30 IF A$="North" THEN GOTO ...
40 IF A$<>"North" THEN GOTO 50
50 IF A$="North-west" THEN GOTO ...
60 IF A$<>"North-west" THEN GOTO 70
70 IF A$="North-east" THEN GOTO ...
80 IF A$<>"North-east" THEN GOTO 10

<> means 'not-equals', and the ... represent further lines which detail the outcome of the inputter's choice.

This simple piece of code is all about covering eventualities and anticipating the flow of logic, which I guess is what is meant by inference. I'm probably straying into dangerous water here, because my knowledge of all things programmy is, as I'm sure is obvious, fairly rudimentary

EG the code has to anticipate not being able to recognise the input, given that a human's response to the initial prompt cannot be anticipated. If the 'not-equal' lines are removed, then the computer or whatever is running the program will not be able to react to an 'input recognition failure' (which I'm sure must have a specific technical term...) and will not be able to fulfil the conditions properly, as it will not know where (ie which line of the program) to progress to.
Is this inference, just so I'm not drifting wildly off-topic?

Sounds great

Perhaps you include some examples where people don't trust in correctness, or the measures to prove it, or trusted wrong. I'm thinking of things like
- the failure in the first flight of Ariane 5 (software error which propagated through different computers)
- modern aircraft or spacecraft with 3 computers of different brands, with software written in different languages which cross-check their results.

* ummm, I should perhaps continue with that 'endless loops' entry *

inference here means logical inference.

IE, given that A is true, you can 'infer' that B is true.

EG, Given that my name is Lucinda, you can infer that I am female, using the *rule of inference* "People named Lucinda are female".

This is also an example of incorrect rules of inference leading to false statements being inferred...

Does that make it any clearer?

--

all typos fixed.

Re: 'assertion' section: I think you're talking about debugging code within the code and/or about profilers, those pieces of software which, apart from measuring execution times, also ensure that assertions are true and that /every/ line of code has been executed at least once. As I said, profilers are /software/ as well, so there's the need for a pro-profiler which checks the correctness of the profiler code...

...GOTO LABEL 1

hehe, simulpost!

Final section "What Else?" added, as per Bossel's suggestion.

Used blockquotes to distinguish between programs and the rest of the text - this might make things clearer...

Assertions can be used for run-time debugging, as you mention - and these are effectively the same as assertions used by proof compilers to generate verification conditions. The former grew out of research in the latter, just as the use of runtime checking of pre and postconditions grew out of research on correctness.

Profilers are an entirely seperate issue...

Ah. Given my previous posting and the responses thereto, I infer that I'd be better off sticking to spelling corrections.

Thanks for the test complaint. It has been processed, edited and passed by Peta.

stuff on inference and axioms and assertions clarified (I hope)

Well, this entry was certaily corrrect Yes, it's been chosen to become part of the edited guide. Congratulations! It should appear sometime in the near future, so watch the front page for it!

J

Editorial Note: This thread has been moved out of the Peer Review forum because this entry has now been recommended for the Edited Guide.

If they have not been along already, the Scout who recommended your entry will post here soon, to let you know what happens next. Meanwhile you can find out what will happen to your entry here: http://www.bbc.co.uk/h2g2/guide/SubEditors-Process

Congratulations!