Re: Use of DBC as "executable SRS": scaling problems

[Nick Leaton <nickle@calfp.co.uk>]

Ken Garlington wrote:

[snip]

> > 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.
> 
> "Executable," unfortunately, doesn't help the reviewer, which was the
> subject of my discussion. It also doesn't help if the invalid input is
> not seen prior to operation.
> 
> I don't know exactly what you mean by "transparent," but I assume you
> mean "easy to read." However, that's not the issue. Consider the
> proposed Ariane-5 Eiffel solution. The assertion #3 ( X <= Maximum )
> is certainly easy to read. Now, prove whether or not X _will_
> exceed Maximum for the Ariane-5. That's much more complicated,
> since there may be a great deal of complexity hiding between the
> system environment inputs and the value of X when it reaches this
> assertion. Note that assertion #1 may be based on different criteria
> than #3, so #1 may pass while #3 fail. So, adding more assertions
> doesn't help here; in fact, it dilutes the review effort.

By transparent in the case of Eiffel assertions I mean that they
are clearly visible to the reader of the code. 

1) They are in set places
2) They are in the code
3) They have a standard form (logical expression)

Compare this to the situation where they are in some other
documentation.

1) They are not in set places. They may be on one project, but they
   are not in set places for all projects

2) They may be in the code, but as comments.

3) They don't have a standard form. They probably are in English.      
   English is prone to ambiguity. Having coded assertions in any
   language a least make sure they compile, and so are in some
   standard form.

So Eiffel helps 1 and 2. 3 is applicable to any language.

> >
> > > > 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?
> 
> Actually, there are such techniques. Failure Modes and Effects Testing
> is very powerful for determining systems that are missing critical
> fault-detection and fault-tolerance requirements, for example.

Nothing stops you using this.


Coming back to the general point, DBC only adds to the software
development process. It is optional. However, I do agree with Meyer in
that you ignore it at your peril. If you are worried about timing being
critical, which is the only valid point that I have read, I have some
concerns. Writing safety critical software where getting something to
work within a set period, and you don't have a large safety margin to
spare worrying. Similarly if you have to rely on software timings
extensively. Getting faster chips strikes me as a better idea, or
waiting till they become available. If you can't, you have a research
project not a production system.

I would be interested in knowing more about the patterns that you use
to handle exceptions when they happen.

-- 

Nick