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

[Olwen Morgan]

I don't think there was such a formal specification. The routine's 
required behaviour was to exhibit good statistical properties over 
repeated invocations. It seems to me perfectly legitimate to regard this 
as a functional black-box requirement. Though it is easily checkable 
with UT, it is not, AFAI can see, one that could even be *captured* in 
the SPARK tools (Rod C, please shoot me down if I'm wrong.) In fact, in 
Wichmann and Hill's paper on their updated, 4-sequence, 32-bit version 
of the algorithm, they state towards the end of the paper that they 
could not actually produce a SPARK compliant coding for it in Ada 
because it maintains an internal state that varies from invocation to 
invocation.

The relevant paper can be downloaded from:


https://www.researchgate.net/publication/220055967_Generating_good_pseudo-random_numbers 



Olwen


On 10/07/2020 13:14, Martyn Thomas wrote:
>
> I shall be interested to see the formal specification against which 
> 'correctness' could be assured. I suspect there may be a category 
> mistake here.
>
> Martyn
>
> On 10/07/2020 13:04, Roderick Chapman wrote:
>> On 10/07/2020 00:36, Olwen Morgan wrote:
>>> 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.
>>
>> I can help with that... we can set it up in my GitHub account and 
>> share results here.
>>
>>  - Rod
>>
>>
>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
> _______________________________________________
> 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/74372c4f/attachment.html>