<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>On 06/07/2020 19:36, Olwen Morgan wrote:<br>
</p>
<blockquote type="cite"
cite="mid:6e996f0f-65d1-3cfd-a127-495f27f2be41@phaedsys.com">I
regard the notion of "rigorous inductive proof" as meaningless in
this context. I have difficulty with the application of the term
"rigorous" to testing since it invites, IMO, a false comparison
with the rigour with which CbyC proofs are carried out. My own
personal practice is, as I have said, to code my units such that
any set of tests that achieves 100% strong, robust, boundary value
coverage (taking both formally-referenced-black-box and
white-box-internal data into account) also achieves 100% simple
path coverage. This is to assure a very high-level of relevant
coverage in testing and typically involves a
pseudo-single-assignment style in which every variable is declared
in the smallest possible scope, is initialised at declaration and
is threatened by assignment in at most one point in its scope. It
tends to resemble functional programming in structure and is
indeed intended to do so on the assumption (possibly unwarranted)
that it tends to make life easier for any prover. This is a major
consideration in C where, if you are striving for best attainable
practice, you might be using several different verification tools.
AFAI can see, this is a far stronger requirement than I've ever
heard anyone else use or advocate. If this was what CARH was
getting at in the notion of "rigorous inductive proof", then
that's what I'm doing. I reached this practice as a result of
developing a somewhat technically paranoid mindset when working in
C system development.
</blockquote>
<p>Here's the extract from the 1969 NATO Software Engineering
conference where Tony Hoare made that remark. Hoare is followed by
a sceptical Perlis. It's helpful that Hoare, Dijkstra and others
are able to join in our discussions so pertinently, half a century
later, though I find it profoundly depressing that the same
discussion is still needed.</p>
<p>Martyn<br>
</p>
<p> </p>
<div class="page" title="Page 16">
<div class="layoutArea">
<div class="column">
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Hoare: </span><span style="font-size:
10.000000pt; font-family: 'Times'">One can construct
convincing proofs quite readily of the ultimate futility
of exhaustive testing of a program
and even of testing by sampling. So how can one proceed?
The role of testing, in theory, is to establish the base
propositions of an inductive proof. You should convince
yourself, or other people, as firmly as possible that if
the program works a certain number of times on specified
data, then it will always work on any data. This can be
done by an inductive approach to the proof. Testing of the
base cases could sometimes be automated. At present,
this is mainly theory; note that the tests have to be
designed at the same time as the program and the
associated
proof is a vital part of the documentation. This area of
theoretical work seems to show a possibility of practical
results, though proving correctness is a laborious and
expensive process. Perhaps it is not a luxury for certain
crucial areas of a program.
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Perlis: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">Much
of program complexity is spurious and a number of test
cases properly studied will exhaust the testing
problem. The problem is to isolate the right test cases,
not to prove the algorithm, for that follows after the
choice
of the proper test cases.
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Dijkstra: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">Testing
shows the presence, not the absence of bugs.
</span></p>
<p><span style="font-size: 10.000000pt; font-family:
'TimesNewRomanPS'; font-style: italic">Lucas gave a brief
summary of the Vienna method (see P. Lucas and K Walk: “On
the formal description of
PL/1” Annual Review in Automatic Programming, Vol. 6). He
gave an example of an application of the Vienna
method, which revealed an error in the mechanism for
dynamic storage allocation of AUTOMATIC variables in the
F-level PL/I compiler (see P. Lucas: “Two constructive
realizations of the block concept and their equivalence”
TR 25.085; also W. Hanahpl: “A proof of correctness of the
reference mechanism to automatic variables in the
F-Compiler” LN 25.3.048; both of which are available from
the IBM Vienna Laboratory).
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Lucas: </span><span style="font-size:
10.000000pt; font-family: 'Times'">The error was not found
by the compiler writers; it was not found by product test
and it would not easily have
been found by any random tests. I am quite convinced that
making this proof was cheaper than the discussions
I have heard among highly-paid people on whether or not
this allocation mechanism would cover the general
case.
</span></p>
<p><span style="font-size: 10.000000pt; font-family:
'Helvetica'; color: rgb(100.000000%, 100.000000%,
100.000000%)">22
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Galler: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">I
think this relates to a common mathematical experience;
when you cannot prove a theorem very often the
sticking-point is the source of the counter-example.
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Llewellyn: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">How
often in practice do these obscure errors turn up?
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Lucas: </span><span style="font-size:
10.000000pt; font-family: 'Times'">Nobody knows how often
these cases turn up; that is just the point. A compiler
writer is not a prophet of all
computer users. Secondly, even if only one user meets the
error it causes him a real problem and it causes a full
system update mechanism to go into action. Even for only
one such case, it is cheaper to make the proof than
mend the bug.
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Galler: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">Engineers
use the “worst case” approach to testing. Has this been
done in software?
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Lucas: </span><span style="font-size:
10.000000pt; font-family: 'Times'">I can’t see any
possibility of specifying worst cases in this kind of
field.
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Reynolds: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">The
difficulty with obscure bugs is that the probability of
their appearance increases with time and with
wider use.
</span></p>
<p><span style="font-size: 10.000000pt; font-family:
'TimesNewRomanPS'; font-style: italic">Dijkstra described
some basic features of his work over the past several
years on the problem of making programming an order of
magnitude easier and more effective. This is described in
full in his working paper in section 7.4.
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Perlis: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">Do
you think the methods you have developed can be taught to
those programmers who have always coded
first and justified last?
</span></p>
<p><span style="font-size: 10.000000pt; font-family: 'Times';
font-style: italic">Dijkstra: </span><span
style="font-size: 10.000000pt; font-family: 'Times'">No
one survives early education without some scars. In my
experience, the intellectually degrading influence
of some educational processes is a serious bar to clear
thinking. It is a requirement for my applicants that they
have no knowledge of FORTRAN. I am not being facetious.
</span></p>
</div>
</div>
</div>
</body>
</html>