[SystemSafety] Correctness by Construction

[andrew at andrewbanks.com]

On 2020-07-13 14:31, Peter Bernard Ladkin wrote:
> On 2020-07-13 14:59 , Michael Jackson wrote:
>> Hoping for illuminating replies, I ask an open question.
>> 
>> In the phrase "Correctness by Construction", what does 'correctness' 
>> mean?
> As I use the term, source code SC is developed CbyC, it means
> 
> * there is a Requirements Specification RS which allows one
> practically to determine whether certain
> program behaviours fulfil it or not
> 
> * there is a means Chk of determining whether program behaviours will
> satisfy RS through analysis of
> the source code SC of the program and the meaning of SC. (This
> statement assumes Chk is sound.)
> 
> * Chk is incremental, that is, it may be applied soundly to source
> code as it is being written, and
> relatively comprehensive, that is, it can be applied to most programs 
> SC
> 
> * SC is indeed developed with incremental use of Chk
> 

But surely, at some stage, "Correctness" can only be actually proven by 
EXECUTING that code on the target hardware.

There are nuances and subtleties that can only ever be truly discovered 
by running the code it its true environment.


A