<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<p>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.</p>
<p>The relevant paper can be downloaded from:</p>
<p><br>
<a class="moz-txt-link-freetext"
href="https://www.researchgate.net/publication/220055967_Generating_good_pseudo-random_numbers">https://www.researchgate.net/publication/220055967_Generating_good_pseudo-random_numbers</a>
<br>
</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 10/07/2020 13:14, Martyn Thomas
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:1c74535a-c2ea-70ea-13c2-43a8ceffae73@72f.org">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<p>I shall be interested to see the formal specification against
which 'correctness' could be assured. I suspect there may be a
category mistake here.<br>
</p>
<p>Martyn<br>
</p>
<div class="moz-cite-prefix">On 10/07/2020 13:04, Roderick Chapman
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:7454a85d-3c4d-4bd4-3357-4cfc00dad1ef@proteancode.com">
<meta http-equiv="Content-Type" content="text/html;
charset=UTF-8">
<div class="moz-cite-prefix">On 10/07/2020 00:36, Olwen Morgan
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:221a3e19-85c7-54b4-a89c-a0671d85307a@phaedsys.com">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.</blockquote>
<p><font size="+1">I can help with that... we can set it up in
my GitHub account and share results here.</font></p>
<p><font size="+1"> - Rod</font></p>
<p><br>
</p>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
The System Safety Mailing List
<a class="moz-txt-link-abbreviated" href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" moz-do-not-send="true">systemsafety@TechFak.Uni-Bielefeld.DE</a>
Manage your subscription: <a class="moz-txt-link-freetext" href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" moz-do-not-send="true">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></pre>
</blockquote>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
The System Safety Mailing List
<a class="moz-txt-link-abbreviated" href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE">systemsafety@TechFak.Uni-Bielefeld.DE</a>
Manage your subscription: <a class="moz-txt-link-freetext" href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></pre>
</blockquote>
</body>
</html>