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-7-bit X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: Peter Horan Subject: Re: A DBC experience (was Re: Design by Contract) Date: 1997/08/29 Message-ID: <34060C4D.AF2@deakin.edu.au>#1/1 X-Deja-AN: 268835996 References: <33E9ADE9.4709@flash.net> <33F133D7.71AC@erols.com> <33F25933.7F83@flash.net> <33F30341.19F7DDE6@calfp.co.uk> <33F832E2.D5322D28@munich.netsurf.de> <33FA7611.4E16@flash.net> <33FB8974.97D4BA5D@munich.netsurf.de> <33FFA82E.54A8@flash.net> <34023A1F.41C67EA6@eiffel.com> <34023BC4.2781E494@eiffel.com> <34026DE7.7D07@pseserv3.fw.hac.com> <3402C404.56812AFB@XYZZYcalfp.com> <5tvfdt$79g@inet-server.sit.fi> <34050D8B.569F@deakin.edu.au> <34056C8C.5520EFE6@XYZZYcalfp.com> Organization: School of Computing and Mathematics, Deakin University Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-29T00:00:00+00:00 List-Id: Richie Bielak wrote: > > Peter Horan wrote: > > > The problem is a side effect which must be present (by inference) in the > > original java code `ecs[i].ready()'. > > No. "ready ()" is a query. There is no side-effect,just concurrency. The socket > can be checked and show as not ready, > but can become ready by the time the postcondition is evaluated. > > This is not really relevent. As the contract states that the socket returned > should be ready for I/O, it doesn't care which socket it is. The contract also > allows result of -1, that is no ready sockets, when in fact a socket has become > ready after all were checked. In the context of our program this was what we > expected. > Agreed. What I should have said was that the post-condition (Result /= -1) implies ecs.item(Result).ready is satisfied if Result = -1. regardless of the value of ecs.item(Result).ready So the argument raised by holsti@ssf.fi fails: > ..UNLESS the socket happens to become ready AFTER it was tested inside the > routine, but BEFORE the postcondition is checked. Granted that in this > example this would be unlikely to occur during the test, but in other > examples similar things might be likely. Holsti also says: > If I understand the Eiffel code > correctly, the postcondition is not sufficient to show that there is no > error in the routine, although it is sufficient to ensure that > the program does not block on a non-ready socket. I am not sure what this means. How is the post-condition insufficient? -- Peter Horan School of Computing and Mathematics peter@deakin.edu.au Deakin University +61-3-5227 1234 (Voice) Geelong, Victoria 3217, AUSTRALIA +61-3-5227 2028 (FAX) http://www.cm.deakin.edu.au/~peter