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

[Roderick Chapman]

On 10/07/2020 13:53, Olwen Morgan wrote:
> 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.)

You're almost certainly right. I don't know how to specify "this stream 
of data is statiscally random" in SPARK - the contract language in SPARK 
is just not set up to express that kind of property.

BUT... given an implementation in SPARK, I would always seek to prove 
type-safety (and possibly termination) of the code, and leave proving 
randomness to a statisitcal UT effort. That would be fine with me.

I don't see a big deal here.  We (meaning my colleagues and predecessors 
at Praxis and SPARK team) have never advocated for the complete removal 
of all dynamic verification activities. Rather, we noted (particularly 
arising from the SHOLIS project in the late 90's) that traditional "one 
unit at a time" testing did not produce useful results for a reasonable 
effort on units that were coded and already verified using SPARK. 
Requirements-based integration and system testing remain absolutely 
vital though - an approach deployed on later projects like MULTOS CA, 
Tokeneer, and iFACTS.

The effort-per-defects-found data for SHOLIS are in IEEE Transaction on 
Software Engineering in August 2000 IIRC.

So... for your random number generator, I suggest we implement it in 
SPARK and see what mix of static and dynamic verification works best.

> 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.

They probably tried to code it as a _function_ in SPARK95. Not a good 
idea, since functions are side-effect free in SPARK, and PRNG algorithms 
tend to be stateful. It will need to be a procedure... no big deal.

  - Rod