From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII X-Google-Thread: fac41,9a0ff0bffdf63657 X-Google-Attributes: gidfac41,public X-Google-Thread: 1108a1,9a0ff0bffdf63657 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,9a0ff0bffdf63657 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,4b06f8f15f01a568 X-Google-Attributes: gid103376,public From: Jean-Marc Jezequel Subject: Re: Software landmines (loops) Date: 1998/09/07 Message-ID: <35F38E1F.4465E6A8@irisa.fr>#1/1 X-Deja-AN: 388627559 Distribution: world Content-Transfer-Encoding: 8bit References: <902934874.2099.0.nnrp-10.c246a717@news.demon.co.uk> <6r1glm$bvh$1@nnrp1.dejanews.com> <6r9f8h$jtm$1@nnrp1.dejanews.com> <6renh8$ga7$1@nnrp1.dejanews.com> <6rf59b$2ud$1@nnrp1.dejanews.com> <6rfra4$rul$1@nnrp1.dejanews.com> <35DBDD24.D003404D@calfp.co.uk> <6sbuod$fra$1@hirame.wwa.com> <904556531.666222@miso.it.uq.edu.au> <35EAEC47.164424A7@s054.aone.net.au> <35EFD468.BDD7CB0A@irisa.fr> <2QVyPDAWkD81Ew70@radm.demon.co.uk> To: Richard Melvin Content-Type: text/plain; charset=iso-8859-1 Organization: Irisa, Rennes (FR) Mime-Version: 1.0 Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada Date: 1998-09-07T00:00:00+00:00 List-Id: Richard Melvin a �crit: > > In article <35EFD468.BDD7CB0A@irisa.fr>, Jean-Marc Jezequel Marc.Jezequel@irisa.fr> writes > > > Nice proof. > > Unfortunately your code contains at least one, and arguably two, bugs: Absolutely. I was interrupted while writing this message just before writing initialization code, and resumed it back only hours later, just before leaving for the week-end. And this stupid computer took what I wrote, not what I meant ;-) Usual problem for many of us. > - will throw an exception or return wrong result on unequal > length lists. True. > > Result := l.first /= r.first Was meant to be Result := l.count /= r.count (copy paste error). > - will interfere with iteration over lists in the calling function > (unless the language you are using passes lists by value, > not identity). true again. There is even another error in it, that magically disappears in step 6 (exercice left to the reader. Hint: the code is correct, the proof is correct, still there is an error. See last line of this message for another hint.) > I've got a theory as to the people writing strict single/entry single > code are having such a hard time with this (defect rate > 20%): I have no theory on that. Was just showing why Dijkstra insisted on se/se loops: in this way programs can be made provable. Sorry guys for my sloppiness in the actual showing. BTW, it illustrate another of my points: don't rely on hand-made proofs *only* (even when you take care of not doing any error in the proof, how can you proove that what you wrote correspond to your *intent*?). -- Jean-Marc Jezequel Tel : +33 299 847 192 IRISA/CNRS Fax : +33 299 847 171 Campus de Beaulieu e-mail : jezequel@irisa.fr F-35042 RENNES (FRANCE) http://www.irisa.fr/prive/jezequel