Re: Interresting thread in comp.lang.eiffel

["Ken Garlington" <Ken.Garlington@computer.org>]

"Joachim Durchholz" <joachim dot durchholz@halstenbach.com> wrote in message
news:8kt18p$36aor$1@ID-9852.news.cis.dfn.de...
> 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. 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? It shouldn't be, since the purpose of OBC_read_value is to
get this parameter off the bus. So, this makes no sense. Are you saying that
this is an output of OBC_read_value (or a mapping to a memory-mapped
variable)? This is correct, although I thought that the "ensure" statement
was the one that was enforced as a post-condition, whereas "require" was a
precondition. If "require" statements are enforced on output (or on access
to memory-mapped values), then the only problem is that "some_maximum_value"
is ALWAYS 32,767. That's what scaling does: It converts floating-point
numbers to a scaled integer value, typically using the maximum precision
available (that is, the smallest floating point number expected is converted
to -32,768, and the largest expected value is converted to 32,767, at least
for a 16-bit bus as in the case of Ariane 5). Therefore, all your "require"
or "ensure" contract says is that the bus is a 16-bit bus. This is useful if
the architecture changes, and the bus grows (or shinks, although this is
unlikely) in bit width. However, it has absolutely no utility in checking
individual bus parameters. In other words, your contracts will always pass,
so long as the bus stays the same.

If scaling were not used, then your contract would potentially have more
value. However, if scaling weren't used, then the specific error encountered
by the SRI would have been avoided. The SRI was in the act of scaling
horizonal_bias to put it on the bus when the overflow occured. (The word
"expected" in the paragraph above is key to understanding the problem.)

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

> 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.
>
> Regards,
> Joachim

OK, although I would hope that you're defending *your own* thinking as a
rule...