[SystemSafety] Correctness by Construction

[Olwen Morgan]

On 15/07/2020 15:23, Martyn Thomas wrote:
> On 15/07/2020 10:49, Peter Bishop wrote:
>
>> The "correctness" achieved by CbyC  does not guarantee that the
>> requirements assigned to the software will address the real world problem.
> I'm not aware of anything that "guarantees" this. It's not obvious to me
> that it is even theoretically possible.

I'm not convinced it's theoretically possible either - witness my 
"Gödelian oddities" programs.

My dominant perspective on this is that *best practice is when your 
tools and methods maximise your chances of detecting errors at the 
earliest possible opportunity to do so*. CbyC is as good as it gets for 
ensuring formal correctness of code wrt. specifications. But that's all 
it can do. There's an awfully large class of errors that it cannot detect.


Olwen