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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,c59f452174bd555
X-Google-Attributes: gid103376,public
X-Google-Thread: fac41,c59f452174bd555
X-Google-Attributes: gidfac41,public
From: Nick Leaton <nickle@calfp.co.uk>
Subject: Re: Use of DBC as "executable SRS": scaling problems
Date: 1997/08/11
Message-ID: <33EF20DF.5390@calfp.co.uk>
X-Deja-AN: 263537051
References: <870209420.19031@dejanews.com> <33DF0010.3545@calfp.co.uk>
 <33E0A26B.1630@flash.net>
X-NNTP-Posting-Host: calfp.demon.co.uk [158.152.70.168]
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-08-11T00:00:00+00:00
List-Id: <comp.lang.ada>


Ken Garlington wrote:
> 
> Nick Leaton wrote:
> >
> > Divide and conquer still applies. One would hope that the component
> > pieces of your system will still small. Using assertions at this level
> > is an advantage.
> 
> Unfortunately, "divide and conquer" leaves open the issue of interface
> validation. In addition to showing the components are valid internally,
> you must also show their interactions are valid. DBC may be able to
> detect (at run-time) when an invalid interaction occurs, but to
> _prevent_
> the invalid interaction requires much system-wide knowledge. This is
> particularly true of the Ariane 5 case, where something *outside the
> system* (the flight profile) was the root cause of the error. Consider
> a chain of events like:
> 
>         environment generates change
>         sensor senses change
>         I/O device reads sensor
>         software gets value from I/O device
>         software does set of calculations (including generation of error term)
>         error term is converted to output format [failure here]
> 
> To determine that the failure would occur, the manual reviewer must
> consider the full chain to trace the relationship of the environment
> definition
> to the out-of-range conversion. This is easy during execution (assuming
> you
> have a good definition of the environment), but hard for a human. And
> you have
> to do this for every thread (more or less). No one will tell you in
> advance
> "the error term conversion is where the error is, now just figure out
> why."

I think I get your logic. Where would you expect the error to be raised?

1) Getting the value? (Postcondition)
2) Sending the value to the calculator (Precondition)
3) In the conversion routine (Precondition)

I would believe you should be writting all. In practice they are
probably written
by different people, so make the assumptions transparent and executable
is good
practice.

....


> > 2) Writting assertions forces you to consider if the requirements
> >    are well formed. If you can't write an assertion, has the requirement
> >    been stated in an unambiguous way? Is it realisable? etc ...
> 
> However, they cannot usually detect _missing_ requirements (Ariane 5
> case).

Yes. Do you have a method that does?

> > 3) There are requirements that cannot be coded as assertions. For
> >    example a bank may have a requirement that the software should
> >    try and prevent the bank becoming bankrupt. Perfectly normal
> >    requirement. The software can help perform this task. However,
> >    stated as such, you cannot code it. You have a problem testing it.
> 
> Actually, it's pretty easy, assuming you have a good definition of the
> bank environment and can run adequate scenarios. It is difficult, on the
> other hand, to have a system be able to internalize all of the factors
> regarding its environment (no system can fully describe itself, much
> less
> itself and its environment!)

Hmmm, ok so we are now on to my home ground, even though I'm a pilot.
It isn't to code up these requirements, even running scenarios which
some banks
do (like the one I work for! ;-) ) Main reason is that it is very hard
sometimes to
come up with a workable set of assumptions on which to base your
scenarios. 
Lots of banks have lossed lots of money making assumptions that are not
valid.

> > 4) Is having assertions on utility classes and verifying them, writing
> >    requirements for them a problem?
> >
> > >     In the end, you would have a *very large* number of assertions to keep
> > >     track of and update as the system's requirements changed. Making sure
> > >     that the changes in your requirements baseline get into the assertions
> > >     correctly would be just as difficult as making sure they get into the
> > >     method bodies correctly, in my view.
> >
> > Again, having the assertions in place, and having the verification and
> > validation performed automatically as you run makes it more likely that
> > you find the errors early rather than latter.
> 
> First, "running" is not early in the development process!

Running the whole system, OK. 'Running' parts of the system? I want
to run my code as quickly as possible, in order to validate the design.
This
is not contrary to 'accepted' practice. I want to develop quickly, so I
want
to get to test quickly.

> Second, it seems that there is a schism in the DBC community. Some feel
> that
> testing (execution of the code) is the important part, while others
> emphasize
> manual verification. It makes it very difficult to discuss the
> advantages of
> DBC, when the response to "it's difficult to manually verify" is "it
> helps catch
> errors during test" and the response to "it's difficult to use
> assertions to test"
> is "it helps catch errors during manual verification."


Manual verification is a weak argument IMHO. However in inspecting code
to 
see what it does in order to use the code, it is very useful. Execution
is
very important. As aid to clear good design, I have found it to be an
excellent
aid to quality code.

> >
> > >     The chance for an error under these conditions is not lessened by DBC.
> >
> > But the impact of it is, as you are more likely to catch it earlier.
> > Remember, you don't have to write the assertions. ie. Eiffel is giving
> > you an extra tool.
> 
> This is the other schism: Arguments about DBC are addressed in Eiffel
> terms,
> and arguments about Eiffel are addressed in DBC terms ("DBC does not
> require Eiffel", for example).
>

Agreed, it just makes it easier to produce code with DBC, and so you are 
more likely to produce code containing the assertions. DBC in C++ is
very awkward,
and from what I have been reading about ADA, the situation is vastly
superior to 
C++, but there are some drawbacks for replication the inheritance of
assertions. 
(see some previous messages)

Out of interest, do you think DBC is a bad concept, or are your
arguments mainly
a C++ vs Eiffel or anti the Ariane article?

> >
> > > (2) If DBC were used as an "executable SRS", the number of assertions in
> > > the
> > >     system could very easily grow so large as to cause deadlines to be
> > > missed.
> >
> > Assertions are inherited. It is common for base classes to have lots of
> > assertions, deferred features (virtual in C++ parlance). Inherit classes
> > don't have many as they have inherited the assertions.
> >
> > >     I suppose that most Eiffel programmers would write preconditions in
> > > terms
> > >     of public attributes (i.e. require (My_Object.Attr_1 = whatever)), but
> > >     even simple comparisons like this could really add up if there are
> > > enough
> > >     of them. This point is only of concern for developers of large
> > > real-time
> > >     systems.
> >
> > Most assertions are of this form. Checks that a reference is not void.
> 
> However, most requirements are not in this form. Does this mean that
> most
> requirements won't be written as assertions?

I disagree. You may not have a requirement explicitly written in your 
design document. Let us say you have an object from an artificial
horizon,
and that, for arguments sake, it contains three values for pitch, yaw
and bank.
A method/routine that has one of these objects as a parameter has a
requirment
that it is passed such an object. (Existance and type conformity). Not
many requirements documents will explicitly state such a requirment,
although
they may state the requirement that the object is optional if that were
the case.

If your requirements are more complex, then break them down into smaller
requirements,
divide and conquer.

> Furthermore, I can get assertions of this form without DBC/Eiffel (e.g.
> in
> Ada, under any methodology). What's special about DBC if it causes you
> to write code just to get checks you get for free in other languages?

DBC is not language specific. Eiffel as a language makes it easy to use
DBC.

How do you get inheritance of assertions in C++, Ada for free?

> (BTW, this is the third schism. Compare and contrast the arguments by
> other
> DBC/Eiffel advocates that most assertions are "high-level" abstractions,
> making them easier to read. I'm pretty much convinced at this point that
> DBC, like the infamous "object-oriented," can mean just about anything
> to
> anyone!)

I agree with the point about high-level nature of assertions. Looking
though
code that I have written this is the case. Classes with a large number
of 
assertions are abstract base classes of heirachies. This is not
surprising.

...

-- 

Nick