<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Olwyn,</p>
<p>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?</p>
<p>Cheers David<br>
</p>
<pre class="moz-signature" cols="72">David Crocker, Escher Technologies Ltd.
<a class="moz-txt-link-freetext" href="http://www.eschertech.com">http://www.eschertech.com</a>
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486</pre>
<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">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<p><br>
</p>
<p>A quick response to Jonathan and Jean-Louis (on my way back to
bed from the bathroom):<br>
</p>
<p>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:<br>
</p>
<p>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]<br>
</p>
<p>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.</p>
<p>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.</p>
<p>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.</p>
<p>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.<br>
</p>
<p>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.<br>
</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 09/07/2020 20:54, jean-louis
Boulanger wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CADO7T_980RC17=JaEbqwmczaynDW0C5rd_WKSbbja=KjdGY1Fw@mail.gmail.com">
<meta http-equiv="content-type" content="text/html;
charset=UTF-8">
<div dir="ltr">
<div class="gmail_default" style="font-size:large">please show
it ...</div>
<div class="gmail_default" style="font-size:large"><br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">Le jeu. 9 juil. 2020
à 21:42, Olwen Morgan <<a
href="mailto:olwen@phaedsys.com" moz-do-not-send="true">olwen@phaedsys.com</a>>
a écrit :<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><br>
A propos of my disagreement with PBL ...<br>
<br>
If anyone's interested, I think I have an example of a
single, small <br>
code unit for which compliance with functional requirements
would be <br>
beyond a SPARK-equivalent verifier and is susceptible to
verification <br>
*only* by real or simulated unit testing.<br>
<br>
<br>
FWIW,<br>
<br>
Olwen<br>
<br>
<br>
_______________________________________________<br>
The System Safety Mailing List<br>
<a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE"
target="_blank" moz-do-not-send="true">systemsafety@TechFak.Uni-Bielefeld.DE</a><br>
Manage your subscription: <a
href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><br>
</blockquote>
</div>
<br clear="all">
<div><br>
</div>
-- <br>
<div dir="ltr" class="gmail_signature">Mr Jean-louis Boulanger</div>
</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>