Please try the URL privacy information feature enabled by clicking the flashlight icon above. This will reveal two icons after each link the body of the digest. The shield takes you to a breakdown of Terms of Service for the site - however only a small number of sites are covered at the moment. The flashlight take you to an analysis of the various trackers etc. that the linked site delivers. Please let the website maintainer know if you find this useful or not. As a RISKS reader, you will probably not be surprised by what is revealed…
Dave Benson nicely identifies a distinction between becoming obsolete
and wearing out, and argues that only the former applies to software.
There is another effect that isn't exactly captured by the words "to
become obsolete." A high quality piece of software, carefully
designed and debugged by an expert, is turned over to a less-skillful
operations team which installs it, runs it--and adds minor field
modifications. As time goes on users of the software notice that it
is no longer bug-free, because the less-skillful modifiers have been
screwing it up. It isn't appropriate to say that the software became
obsolete; if it hadn't been tinkered with then the term obsolete
might apply.
Since most software does get modified to meet changing conditions of
use, and often those modifications are not done by the original
implementation team, this effect is quite common. If the effect goes
on long enough, it may be necessary to commission a new
implementation, almost as if the original implementation had worn out.
Some people have in mind the impairment and diminished usability
caused by this effect when they use words like "wears out" or "rots".
I guess we need a plain English word for it so that neophytes won't
think that computers that haven't been oiled properly rub too hard
on the bits.
Jerry
1. I have a 1983 Ford with "Cruise Control" 2. I have had a CB in it from the day it was picked up (7/3/83) until the day the CB was stolen (10/2/86). No problems. 3. I put a new, more sophisticated CB in it on 10/4. New CB has an SWR (Standing Wave Ratio) meter, and an "Antenna Warning" light. Both intended to help tune antenna system, and ensure crummy antenna connections don't cause loss of signal strength - or excessive reflection of trans- mitted signal. 4. SWR of 1.0 is perfect, and impossible. SWR of 1.5 is good. SWR of 2.0 is poor. SWR > 3.0 UNSAT! 5. New CB installed with only trivial cursing and sweating. Tuned up just fine. Car drove fine (as before). 6. Rains came. SWR > 3.0. Probable cause bad antenna connections/cable, getting soaked. Cruise control acted up. Wonder why? 7. Car baked in sun. SWR < 2.0. Cruise control OK. 8. This morning, car wet from heavy dew. SWR > 3.0. Cruise control cuts out when microphone is keyed. Every time. 9. Car dries out, SWR < 2.0, Cruise control not affected. 10. SWR ratio must have varied with moisture on old set, same as new. Never had problem before... but did re-route the power cables to new set, more "neatly" than before, i.e., more jammed up behind instrument panel. Conclusion: New CB/re-routed wiring somehow interacts with "Cruise Control" micro, causing it to kick out when SWR is high. At least it "fails safe." N.B.: I don't usually drive in rain with cruise control on, but do use it w whenever safe to do so - saves gas on level-ish interstates. - Mike
In response to utzoo!henry (Henry Spencer):
<> A mathematical proof is, technically, a completely reliable method of
<> ensuring the correctness of programs, ... [from a Hoare quotation]
>I think talk of "total correctness" and "complete reliability" shows excess
>enthusiasm rather than realistic appreciation of the situation.
Agreed.
Henry then compares this notion of proof with the Rourke-Rego "proof" of
the Poincare conjecture, whose status currently is unknown. And as Henry
says, in mathematics
>the specs for the problem are very simple and obviously "right".
I must take exception to this comparison.
Mathematics, believe it or not, works under the Hundredth Monkey Phen-
omenon. Programs do not.
Let me explain.
Proofs in mathematics (at least at the cutting edge) deal with inher-
ently complicated mentally defined objects. It takes a while to get
your mind in sync with whatever it is you are studying. Details and
(not always elementary) claims are left to the reader. The field,
already huge beyond comprehension, would sink under its own weight
otherwise.
New and difficult proofs, like that of Rourke-Rego, take their time to
sink into the mathematical community's collective consciousness. But
once they do, a new level of confidence and ability is reached, and the
proofs become accessible.
The above is not possible with programs. At some point, every detail
must be given, somewhere. There is no reason why a proof-checker could
not be used to check for correctness, matching pre-and-post assertions
with each statement.
So, where do "proven" programs fall down?
First, there really are the incorrect proofs. But I believe this can
be cured. (Of course, relying on a proof-checker could be risky if
*that* program has bugs. But surely that is a low enough operation to
get right. [And now a new {recursive} nightmare comes to mind.])
Second, compilers and hardware do not always match the programmer's
intent. Hidden pointer nonsense, erroneous implementations of math-
ematical functions, silent truncation of overflows, etc. cannot be
checked for unless the programmer is aware of such glitches.
Third, the outside world need not match the programmer's intent eith-
er. The beginning assignment of input, and the final interpretation
of output is outside the program's proof's scope. GIGO, as we all
know.
Fourth, the theoretical process being used may be incorrect or just
inappropriate in a particular situation. One can give your numerical
analysis routines a proof that they do what is wanted, and build your
aircraft or nuclear reactor or what have you with a new false confi-
dence, despite the fact that the case at hand is subject to numerical
instability or similar problems.
So in summary, a program and its proof are meaningful relative to each
other, and nothing else. I would hate to think of the consequences if
someone forgot this when implementing SDI, say.
ucbvax!brahms!weemba Matthew P Wiener/UCB Math Dept/Berkeley CA 94720
>From: decvax!utzoo!henry@ucbvax.Berkeley.EDU >I think talk of "total correctness" and "complete reliability" shows excess >enthusiasm rather than realistic appreciation of the situation... "Total correctness", at least, is a technical term in program verification. "Partial correctness" means that the program does the correct thing iff it terminates (i.e., the program that never terminates is partially correct). Total correctness is, partial correctness together with termination. All of these terms really mean "meets the mathematical specification". >Another cautionary tale is the current debate about the validity of the >Rourke/Rego proof of the Poincare conjecture. As I understand it — it's >not an area I know much about — the proof is long, complex, and sketchy, >and nobody is sure whether or not to believe it. And this is a case >where the specs for the problem are very simple and obviously "right". The proofs of program correctness are (supposed to be) checked by machines. There's been a lot of work done (and even a little success, I think) in getting proof techniques that can be checked automatically, and even ways of getting the machine to do a lot of the drudgework in converting a human-style proof into a machine one. Of course, you have to check the proof-checker... As I understand the area of correctness proofs, there are two major problems: 1) Program specifications (especially complicated ones) rarely specify what you want the program to do. Not a whole lot program verification can do about this. 2) It is very hard to prove a program correct. Loop invariants, for example, are rather hard to come up with. Once you have the proof, it's easy to check. > To borrow from the theme of a PhD thesis here some years ago, proving > programs INcorrect is much easier than proving them correct, I agree. The rumor around here is, the best use of program-proving techniques is in finding bugs. -- Bard Bloom
Please report problems with the web pages to the maintainer