[SystemSafety] More on my contretemps with PBL ...
Olwen Morgan
olwen at phaedsys.com
Fri Jul 10 01:36:35 CEST 2020
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>
More information about the systemsafety
mailing list