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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,a48e5b99425d742a X-Google-Attributes: gidfac41,public X-Google-Thread: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public From: Alan Brain Subject: Re: Simulating Eiffel-style assertions (was: Papers on the Ariane-5 crash and Design by Contract) Date: 1997/03/26 Message-ID: <3339F210.69E3@dynamite.com.au>#1/1 X-Deja-AN: 228463502 References: <5h6jc0$jvu@news.rhrz.uni-bonn.de> Organization: @Home Reply-To: aebrain@dynamite.com.au Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada Date: 1997-03-26T00:00:00+00:00 List-Id: Wolfgang Reddig wrote: > Consider a 'Car' class having an invariant which states that cars have > either two or four doors. Lets assume there is a method 'make_limousine', which > adds two doors (forgive the C++ notation, but I'm not very familiar with > the syntax of Eiffel): > > void Car::make_limousine() > { > require(no_of_doors() == 2) > ensure(no_of_doors() == 4) > > add_door(); // this would (incorrectly) cause an invariant failure! > add_door(); > } But surely there's another way. Consider the following reasoning: Cars, for our purposes, have either 2 or 4 doors, never 3, never 5. So we can have: type CAR_DOOR_NUMBER_TYPE is ( Two, Four ); type CAR_RECORD_TYPE is record -- some data about the car, make, model etc here -- NUMBER_OF_DOORS : CAR_DOOR_NUMBER_TYPE; -- -- and maybe some more data here -- end record; -- then for the code ADD_TWO_DOORS (ToCar : CAR_RECORD_TYPE ) is begin ToCar.NUMBER_OF_DOORS := CAR_RECORD_TYPE'SUCC ( ToCar.NUMBER_OF_DOORS); -- -- or, if you want to 'Fail Safe' -- -- ToCar.NUMBER_OF_DOORS := Four; -- exception when CONSTRAINT_ERROR => -- There already WERE Four Doors! -- if you want to 'Fail Safe' ToCar.NUMBER_OF_DOORS := Four; -- if you want to crash and burn, or destroy the rocket -- raise; when others => -- Has to be a hardware problem, or some -- C program overrunning its array bounds, -- or a bug in the compiler - null; -- Try keeping fingers crossed and hoping -- for the best? end ADD_TWO_DOORS; No apologies for the Ada-83 syntax. Ada supplies the tools to "Judo" the problem, avoid the concept of a 3-door car from being expressible. But as Ariane-5 showed, having the capability to do this /= actually doing it. C++'s enums appear similar, but that's another matter. -- aebrain@dynamite.com.au <> <> How doth the little Crocodile | Alan & Carmel Brain| xxxxx Improve his shining tail? | Canberra Australia | xxxxxHxHxxxxxx _MMMMMMMMM_MMMMMMMMM 100026.2014 compuserve o OO*O^^^^O*OO o oo oo oo oo By pulling MAERKLIN Wagons, in 1/220 Scale See http://www.z-world.com/graphics/z/master/8856.gif for picture