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