[SystemSafety] More .....

[Olwen Morgan]

On 10/07/2020 15:11, Peter Bernard Ladkin wrote:
>
> On 2020-07-10 14:53 , David Crocker wrote:
>>
>> The statistical correctness of the code sounds to me beyond the realm of automatic verification;
> Coals to Newcastle, maybe, but CbyC, and use of FM, does not depend on *automatic* verification.

Practical use of CbyC *does* depend on automatic verification. Would you 
claim to be a good enough wrangler to do the proof of 100k lines of 
SPARK Ada manually overnight?

Besides, my point was that the SPARK CbyC method *cannot even capture 
the statistical requirements* on a PRANG - as, AFAI can make out, Rod C 
has confirmed in a recent posting.

>
> If you have code whose output is asserted/desired to have certain statistical properties, such as a
> pseudo-random number generator, then in principle you can run Monte Carlo simulations sufficient to
> determine to a given confidence (not 100%) that the output has those properties.
>
> That is just as much a FM as anything else, and it is just as much a proof as anything else.

OK, we seem to have got to the bottom of at least part of the 
misunderstanding. In my understanding of the CByC/UT boundary, I took it 
that formal verification without running the code was part of the CbyC 
bit and anything that did involve running the code was part of UT or 
later testing.

> Calling Monte Carlo simulations "unit tests" seems to me to be inappropriate.

*Simulated* MC testing is indeed arguably not UT in the sense that it 
does not run the program. Real MC testing that runs the code is most 
definitely UT. But the difference is much like the difference between 
running the PRANG under an interpreter and running it as compiled code. 
In the case of the Wichmann-Hill PRANG, AFAI can see, simulated testing 
would provide no more assurance than real testing but would probably 
take a lot longer.

And - please excuse my ignorance - which current automatically formally 
verifiable specification/coding formalisms can actually capture the 
PRANG statistical requirement - or for that matter, and to use Michael 
J's terminology, any other "long-span" requirement?


Olwen