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

David Crocker dcrocker at eschertech.com
Fri Jul 10 14:53:04 CEST 2020


Hi Olwyn,

The statistical correctness of the code sounds to me beyond the realm of
automatic verification; but what else do you want to prove about the
code? Have you tried running eCv on the C implementation?

Cheers David

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 10/07/2020 00:36, Olwen Morgan wrote:
>
>
> 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
>
> _______________________________________________
> 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/20200710/9949a282/attachment-0001.html>


More information about the systemsafety mailing list