[SystemSafety] Correctness by Construction

[Peter Bishop]

I would have said "Correctness" is:

"It does what it says on the tin"

i.e. the implementation satisfies the specification (and does not do
anything else)

"It" in this case is the binary code running on the processor hardware.

So a proof of "correctness be construction" e.g. using SPARK, is only a 
partial proof,
i.e. that the Spark Ada implementation is semantically consistent with
the specification
This needs to be supplemented by supporting assumptions, e.g.:

a) The SPARK compiler correctly translates the Ada code to the binary
code of the target processor

b) the hardware execution of the processor is consistent with its
specified semantics

There could be more .. (e.g.  assumptions about  compiler
implementation-dependent language constructs)

Plus, even if we could prove all this, "correct" in this sense does not
mean that
the specified behaviour is actually what is needed for the application.

Peter

On 13/07/2020 13:59, Michael Jackson wrote:
> Hoping for illuminating replies, I ask an open question. 
>
> In the phrase "Correctness by Construction", what does 'correctness' mean? 
>
> -- Michael
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety

-- 

Peter Bishop
Chief Scientist
Adelard LLP
24 Waterside, 44-48 Wharf Road, London N1 7UX

Email: pgb at adelard.com
Tel:  +44-(0)20-7832 5850

Registered office: 5th Floor, Ashford Commercial Quarter, 1 Dover Place, Ashford, Kent TN23 1FB
Registered in England & Wales no. OC 304551. VAT no. 454 489808

This e-mail, and any attachments, is confidential and for the use of
the addressee only. If you are not the intended recipient, please
telephone 020 7832 5850. We do not accept legal responsibility for
this e-mail or any viruses.