[SystemSafety] More on my contretemps with PBL ...
Roderick Chapman
rod at proteancode.com
Fri Jul 10 15:20:37 CEST 2020
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
More information about the systemsafety
mailing list