Re: Simulating Eiffel-style assertions (was: Papers on the Ariane-5 crash and Design by Contract)

[wolfgang@uran.informatik.uni-bonn.de (Wolfgang Reddig)]

In article <3339F210.69E3@dynamite.com.au>, Alan Brain <aebrain@dynamite.com.au> writes:
>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. 

Yes, one can simulate some assertions by subtype constraints. However,
perhaps things get more difficult if you have an invariant clause such as:

   no_of_doors = 4 implies horse_powers > 100

(I hope I got the syntax right).

As for C++ enums: the bad news is that C++ compilers don't initialize
enum data members. If you forget to initialize them in an constructor,
you have arbitrary garbage. Thus, there is no guarantee whatsoever that
the values of enums are in range at runtime.

>-- 
>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
>

Regards,
Wolfgang

+---------------------------------------------------------------------+
|  Wolfgang Reddig                |  e-mail:                          |
|  Institut fuer Informatik III   |  wolfgang@informatik.uni-bonn.de  |
|  Roemerstrasse 164              |                                   |
|  53117 Bonn                     |  Tel.: (49) 228 / 73-4513         |
|  Germany                        |  Fax:  (49) 228 / 73-4382         |
+---------------------------------------------------------------------+