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

[Alan Brain <aebrain@dynamite.com.au>]

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