[SystemSafety] More on my contretemps with PBL ...

[Olwen Morgan]

A quick response to Jonathan and Jean-Louis (on my way back to bed from 
the bathroom):

The example is in fact very simple. It's the Wichmann-Hill 16-bit 
pseudorandom number generator (PRANG) algorithm. Basically, for a 16-bit 
generator, you use three linear congruential generators in each of which 
successive terms are related by a recurrence relation of the form:

t(i+1) = (a * t(i)) mod m for some prime modulus m and coefficient a 
that is a primitive root mod m, where m is in the range [2^14+1, 2^15-1]

For positive values of the t(i) less than or equal to their respective 
moduli, these sequences have statistically short periods and none singly 
provides a statistically very good generator. But if you use 3 such 
generators with different moduli and primitive root coefficients and 
take the fractional part of the sum of each of the three t(i) divided by 
its corresponding modulus at each cycle, then you get a much better 
generator of values uniformly distributed in the interval (0,1). AFAI 
recall, Wichmann and Hill found that that this led to a generator with a 
period of around 2^43 that had very good statistical properties as 
evidenced by its performance on various tests of early 1980s vintage - 
the runs test being the most powerful discriminator.

There is a potential pitfall of 16-bit overflow that you can get if you 
use a modulo operator in the computation but Wichmann and Hill used a 
simple equivalent coding that avoided the problem. AFAI can see, a 
SPARK-like verifier would be able to prove that there was no integer 
overflow - and in fact freedom from runtime error. YET the essential 
functional requirement is statistical quality and that reduces to a 
requirement that the generator be, up to a prescribed level of 
statistical confidence, indistinguishable by testing from a 
corresponding true uniform random source. AFAI can see the only way to 
demonstrate that this functional requirement is met is by simulated or 
real testing of the routine over large numbers of cycles, and then 
running of a quality test on the sequence of generated data values.

Somewhere or other I have code for this generator in C complying with 
C90. I'm sure that it would readily transliterate into SPARK Ada and I'd 
be interested to learn what the capability of the SPARK tools would be 
to prove functional correctness.

Note, of course, that this is quite a special case of a functional 
requirement but I do think it is a valid conceptual counterexample to 
PBL's original statement. AFAI can see, it's an example of required 
functional behaviour that is not captured in the I/O transfer function 
of the generator for each individual cycle and therefore remains 
unprovable by the kinds of methods that the SPARK tools use.

I'll dig out the C code of the example tomorrow. If I'm lucky, I might 
be also be able to find a reference to a later paper by Wichmann and 
Hill that describes a 32-bit PRANG based on 4 linear congruential 
sequences. AFAI recall, that paper actually contained Ada code for the 
generator, so the relevant verification capability of the SPARK tools 
could be investigated simply by SPARKing the Ada.


Olwen



On 09/07/2020 20:54, jean-louis Boulanger wrote:
> please show it ...
>
>
> Le jeu. 9 juil. 2020 à 21:42, Olwen Morgan <olwen at phaedsys.com 
> <mailto:olwen at phaedsys.com>> a écrit :
>
>
>     A propos of my disagreement with PBL ...
>
>     If anyone's interested, I think I have an example of a single, small
>     code unit for which compliance with functional requirements would be
>     beyond a SPARK-equivalent verifier and is susceptible to verification
>     *only* by real or simulated unit testing.
>
>
>     FWIW,
>
>     Olwen
>
>
>     _______________________________________________
>     The System Safety Mailing List
>     systemsafety at TechFak.Uni-Bielefeld.DE
>     <mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
>     Manage your subscription:
>     https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
>
>
> -- 
> Mr Jean-louis Boulanger
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200710/2da9825e/attachment.html>