5-Oct-86 22:48:54-PDT,10164;000000000000 Mail-From: NEUMANN created at 5-Oct-86 22:46:51 Date: Sun 5 Oct 86 22:46:51-PDT From: RISKS FORUM (Peter G. Neumann -- Coordinator) Subject: RISKS-3.76 DIGEST Sender: NEUMANN@CSL.SRI.COM To: RISKS-LIST@CSL.SRI.COM RISKS-LIST: RISKS-FORUM Digest, Sunday, 5 September 1986 Volume 3 : Issue 76 FORUM ON RISKS TO THE PUBLIC IN COMPUTER SYSTEMS ACM Committee on Computers and Public Policy, Peter G. Neumann, moderator Contents: Obsolescence vs wearing out (RISKS-3.75) (Jerome H. Saltzer) Cars, computers and unexpected interactions (Mike McLaughlin) Re: Mathematical checking of programs (quoting Tony Hoare) (Matthew Wiener) "Total correctness", "complete reliability" (RISKS-3.75) (Bard Bloom) The RISKS Forum is moderated. Contributions should be relevant, sound, in good taste, objective, coherent, concise, nonrepetitious. Diversity is welcome. (Contributions to RISKS@CSL.SRI.COM, Requests to RISKS-Request@CSL.SRI.COM) (Back issues Vol i Issue j available in CSL.SRI.COM:RISKS-i.j. Summary Contents in MAXj for each i; Vol 1: RISKS-1.46; Vol 2: RISKS-2.57.) ---------------------------------------------------------------------- Date: Sun, 5 Oct 86 14:14:16 EDT To: RISKS FORUM (Peter G. Neumann -- Coordinator) Subject: Obsolescence vs wearing out (RISKS-3.75) From: Jerome H. Saltzer 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 ------------------------------ Date: Sun, 5 Oct 86 16:33:33 edt From: mikemcl@nrl-csr (Mike McLaughlin) To: risks@csl Subject: Cars, computers and unexpected interactions 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 ------------------------------ Date: Sun, 5 Oct 86 16:00:39 pdt From: weemba@brahms.Berkeley.EDU (Matthew P Wiener) To: risks@csl.sri.com Subject: Re: Mathematical checking of programs (quoting Tony Hoare) 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 ------------------------------ Date: Sun, 5 Oct 86 10:48:52 edt From: Bard Bloom To: RISKS@CSL.SRI.COM Subject: "Total correctness", "complete reliability" (RISKS-3.75) >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 ------------------------------ End of RISKS-FORUM Digest ************************ -------