Re: Interresting thread in comp.lang.eiffel

["Joachim Durchholz" <joachim dot durchholz@halstenbach.com>]

Ken Garlington <Ken.Garlington@computer.org> wrote:
> "Joachim Durchholz" wrote:
> > It's dead simple: If physical parameters (like a horizontal bias)
> > enter into the specifications, they must be modelled.
>
> See, you're already in trouble. Horizonal bias is not a "physical
> parameter", in this case. It's an _output_ of the SRI, derived from
> physical measurements of the environment, not an input.

Arrrgh... do you *ever* read what I say elsewhere, or do I have to
reiterate the *full* reasoning whenever I deal with you?

I assume that the horizontal bias is a physical property, measured by
the IRS and returned by the IRS.
In that case, the IRS has a contract that relates physical bias and
measured bias. (If the IRS has just paper specifications, it's easy
enough to translate them to contracts.)
The general flight control software somewhere, in some way, retrieves
the measured bias from the IRS. Or the IRS spontaneously sends its data,
then there's an interrupt routine that will receive that data. In any
case, there is some software that uses this data; and the programmer of
that line will very likely see the contract. He will also enter this
contract into the contract of the software that he, in turn, is writing,
so the contract will percolate up the software layers, until it is seen
by somebody at a high level who *also* knows the Ariane-5 trajectories.
*If* that high-level programmer looks at the details of these contracts,
*then* the problem would have been detected.

That's a lot of ifs, though none of them is unreasonable given the care
that obviously was general in the Ariane project. That's the reason why
I say that assertions would have helped to detect the inconsistency,
instead of that they would have automatically detected them

> From the OBC (the flight
> control) side, it's a value coming in from a different system, via a
> bus. If it's scaled, then range checks are ineffective (as I noted
> in another post).
>
> > Assertion modelling need
> > not restrict itself to statements on values inside a program, so in
> > the end you'll get a contract like
> >
> >   OBC_read_value: INTEGER is
> >   require
> >     physical_reality.rocket.horizontal_bias <= some_maximum_value
> >   ensure
> >     read_value <= 32767
> >   end
> >
> > This is very different from what you write, and clearly spells out
> > what the parameters are.
>
> It's not clear how you are treating
> "physical_reality.rocket.horizontal_bias" here. Is it an input to
> OBC_read_value?

No. It's physical reality. Or, rather, the specification of physical
reality.
Not computable (except if you program a simulation - and it's a good
idea to have a physical_reality feature with contracts if you ever want
to write a simulation, this would ensure that the simulation and the
flight control software use the same assumptions).

> Perhaps if you posted something a little less vague, such as an
> Ethernet device driver written in Eiffel, I might be able to see
> the utility of your approach...

Adding assertions is work that's proportional to the code size, and
frankly I have spent much more time on this issue than I care.
So, please stop coming forth with proposals how to spend my free time. I
know full well what I can do in it.

> > This is my last post on this issue. I have just been crossed by Mr.
> > Meyer and don't wish to defend his thinking in public anymore.
>
> OK, although I would hope that you're defending *your own* thinking
> as a rule...

Done.
Though I'm not going to spend more time to convince you. You're one
unusually locked-in individual - I see more interest in tearing down the
ideas of others than in evaluating these ideas for their usefulness. (I
also see an above-average ability to express your own ideas, which is
why I've been taking the time, but the effort-to-effect ratio has been
degrading, and I don't wish to bore the audience with repetitions to get
the points across.)

-Joachim
--
This is not an official statement from my employer or from NICE.
Reply-to address changed to discourage unsolicited advertisements.