<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<p>You fail to grasp my point.</p>
<p>Mathematics is not some absolute in a world of forms. Its use in
CbyC software development cannot entirely obviate testing since
its efficacy rests on how closely it describes the behaviour of
the systems with which it deals and on the assumptions it makes
about them.</p>
<p>You are quite right to make the observation about a typed "2"
being taken for a "5". But that merely illustrates the magnitude
of the assumptions, modulo which, proofs provide the claimed level
of assurance. One is relying on, among other things:</p>
<p>(1) The requirements specification permitting the generation of
acceptance tests that give a suitably rigorous exercise of
functional behaviours specified in the requirements.<br>
</p>
<p>(2) Corresponding conditions being met by both the architectural
and detailed design specifications.</p>
<p>(3) A coding process that is designed faithfully to reflect the
software unit specifications and the requirements of verification
tools.<br>
</p>
<p>(4) The correctness of the compilers for all programming
languages used.</p>
<p>(5) The soundness of the verifier's reasoning about what the
compiler will do with the code. (Admittedly far less dubious for
SPARK Ada than, AFAI am aware, for any C verifier supported by any
known subset of C).<br>
</p>
<p>(6) The correctness of test coverage measurement tools.</p>
<p>... to mention only the most salient.</p>
<p>Yes, it is true that when we question things at this level of
detail, we feel we are getting into a Godelian regress (which we
aren't - the regress is finite even if it is large). But that does
not alter the fact that CbyC rests critically on some pretty big
assumptions about the tool chain. Soundly done, CbyC can reduce
the risks of not unit-testing. It cannot eliminate them. If you
get a test failure at the next level up, you still have to check
backwards and accept that you may well find an error in a coded
unit ... or somewhere in the tool chain.<br>
</p>
<p>As regards testing on iFacts, I worked on that project and was
asked at one stage by one of the client's engineers to look into
how well a certain routine had been tested. That particular
routine tracked the movement of military aircraft across
(non-convex) sectors of air space. My conclusion was that to give
a greater degree of confidence that the testing was adequate, the
system should internally partition the airspace into convex
subsets - in this case triangular prisms, because movement across
such subsets is easy to track and the tracking routine
correspondingly easier to test. This upset the engineer who had
specified the airspace model in Z because that model was as
minimal as one could get. As far as I could see it specified a
basis for a topology, which struck me as abstraction shooting
itself in the foot. Why weaken to something weaker than a topology
when, by the process of stereographic projection by which the
airspace was defined, a entire coherent *geometry* was given?
Abstracting away from agreed well-defined geometry hardly
demonstrates mathematical finesse. Needless to say there was a bit
of an atmosphere in the office for a while - not least because the
engineer responsible for that bit of the Z spec was a Cambridge
mathematics graduate (who IMO should have known *a lot* better). I
was eventually told that my comments would be borne in mind if
evidence should arise that the testing of the relevant routines
had in fact been inadequate. NOBODY suggested that my concerns
lacked a sound technical basis.</p>
<p>As regards Altran omitting unit tests, if I were advising a
client on whether I thought it advisable, my own view would be
that it was not. And the reason for this is simple. Errors are
cheaper to correct the earlier you detect them. Not unit testing
runs the risk of detecting errors in units later than might
otherwise have been achieved. In taking that view, I would be open
to arguments about relative risk PROVIDED that I was supplied with
relevant data, details of how the data had been obtained,
specification of the statistical analyses used and convincing
arguments as to the repeatability and reproducibility of the
results that the statistical testing was claimed to support. In
this, I think, I would be taking a view entirely consistent with
sound scientific practice.</p>
<p>My responsibility on iFacts was in providing initial consulting
on a suitable subset of C and corresponding subset enforcement
tools and later myself examining all C checker tool outputs for
each build to ensure that they met the specified requirements. I
ought to point out in that connection, that the software that
paints the AT controller's radar display screen is written
entirely in C using X libraries for which many deviations from the
MISRA C subset were required (an average build required
examination of 12,000 error messages to check that all observed
deviations were permitted ones - though I got this down to 300 by
supervising the development and use of a post-processing tool that
put diagnostic suppression messages at contextually identified
positions in the code, any redundant ones being detectable from
unused suppression reports in the tool output. So much, then for
CbyC in iFacts. ONLY THE ADA BITS WERE CbyC !!!. True, the only
bits in C were as inconsequential as painting the radar display
screens that the ATCs looked at but, if I apprehend you correctly,
that was a minor detail?<br>
</p>
<p>I confess to a degree of skepticism that results largely from my
mixed experiences with C. I would like to see C verifiers used
much more widely. To support efforts in that direction, I have,
some twelve years ago, offered a meta standard allowing C subsets
to be formally defined and tailored to verifier capabilities.
Nobody has taken up the (absurdly simple) ideas that I presented.
Notably, the outstandingly inept MISRA C working group has
resolutely refused to adopt a rigorous specification even of a
subset as weak as MISRA C - and I've been into that sorry story
before on this list. (Their reason: It would "alienate MISRA C's
readership base ... WTF?!)</p>
<p>I'd expect SPARK tools relying on the SPARK language to get
pretty good results. But SPARK developments are not the whole of
software engineering. If unit-testing is found to be dispensable
without risk in SPARK developments, great. Modulo my reservations
above, I'd countenance giving it (heavily) qualified support - or
at least absence of desctructive opposition. Not so for C - nor
for any poorly defined language, with no safety/reliability subset
and no verification tools. In suboptimal conditions, I would never
dispense with unit testing and I question the wisdom of so doing
even in the best conditions currently sustainable.</p>
<p>In the end it's all down to risk and numbers. Give me hard,
*robustly reproducible* evidence that using CbyC makes
unit-testing redundant and I'll consider it. But please do not
expect me to be a pushover when it comes to examination of claims
of reproducibility. I was trained to assess these things to UKAS
standards - which are considerably more stringent than almost any
others - an assessor can raise non-compliance issues based not
only on a tick-the-boxes compliance checklist but also on
fitness-for-purpose in the assessor's considered technical
opinion. When it comes to software engineering processes, I'm not
at all easy to convince.</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 01/07/2020 17:53, Peter Bernard
Ladkin wrote:<br>
</div>
<blockquote type="cite"
cite="mid:68edc810-8a40-2f5d-7943-2cffbcd1dccc@causalis.com">
<pre class="moz-quote-pre" wrap="">
On 2020-07-01 18:25 , Olwen Morgan wrote:
</pre>
<blockquote type="cite">
<pre class="moz-quote-pre" wrap="">
Sorry, Peter, but if I have a choice between believing you and believing Arnold, I'm afraid Arnold wins.
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">Which makes my point better than I could have made it myself.
Which bits of Newton do you believe? The stuff in Principia or the stuff about metals vegetating? Or
gravity being caused by salniter? Why?
PBL
Prof. Peter Bernard Ladkin, Bielefeld, Germany
Styelfy Bleibgsnd
Tel+msg +49 (0)521 880 7319 <a class="moz-txt-link-abbreviated" href="http://www.rvs-bi.de">www.rvs-bi.de</a>
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
The System Safety Mailing List
<a class="moz-txt-link-abbreviated" href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE">systemsafety@TechFak.Uni-Bielefeld.DE</a>
Manage your subscription: <a class="moz-txt-link-freetext" href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></pre>
</blockquote>
</body>
</html>