[SystemSafety] CbyC and unit testing

[Olwen Morgan]

Martyn,

Thank you *very much* for going to the trouble of reproducing this.

Having seen how CARH described "rigorous inductive testing" (RIT), I 
realise that this is indeed my intuitively-reached approach. The 
immediate reply of Perlis to CARH somewhat misses CARH's point, I 
believe. Nonetheless he is right, IMO, in saying that much of program 
complexity is spurious in the sense that very few programmers ever seek 
to find the simplest possible program that satisfies the functional 
requirements (i.e. they do not seek to minimise - and often cannot even 
spell - Kolmogorov complexity). If you use the methods that I have used, 
unnecessary complexity kicks you in the teeth pretty quickly.

Also of note is Perlis' remark about coding first and justifying later. 
I've only ever done this for quickly hacked-together programs mostly in 
scripting languages. As a result when I have completed coding anything 
serious, I have already effectively the outline of the necessary set of 
base tests for CARH's RIT. It has always seemed obvious to me that one 
should work in this way. Although it may seem self-serving to claim it, 
most of of what Dijkstra and Hoare started saying from the late 1960s 
onwards had been obvious to me from very early in my programming career. 
I attribute this to a very unusual school mathematics education over the 
period 1964-1971. Long before most schools started teaching computing, 
my school (St. Dunstan's College) had textbooks on the design and 
working of computers - even for first-form teaching. There was *never*, 
in my mind, any conceptual separation between programming and 
mathematics. I have *always* regarded programs as formal systems that 
should be reasoned about - although I readily admit that this is pretty 
unusual for people of my vintage.

Like you, I am deeply disheartened that our profession seems to learn so 
glacially slowly.


Olwen


On 07/07/2020 15:43, Martyn Thomas wrote:
>
> On 06/07/2020 19:36, Olwen Morgan wrote:
>
>> 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. 
>
> 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.
>
> Martyn
>
> Hoare: 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.
>
> Perlis: 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.
>
> Dijkstra: Testing shows the presence, not the absence of bugs.
>
> 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).
>
> Lucas: 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.
>
> 22
>
> Galler: 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.
>
> Llewellyn: How often in practice do these obscure errors turn up?
>
> Lucas: 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.
>
> Galler: Engineers use the “worst case” approach to testing. Has this 
> been done in software?
>
> Lucas: I can’t see any possibility of specifying worst cases in this 
> kind of field.
>
> Reynolds: The difficulty with obscure bugs is that the probability of 
> their appearance increases with time and with wider use.
>
> 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.
>
> Perlis: Do you think the methods you have developed can be taught to 
> those programmers who have always coded first and justified last?
>
> Dijkstra: 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.
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200707/e3bc9d0e/attachment-0001.html>