<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<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>
</body>
</html>