[SystemSafety] Correctness by Construction

[Peter Bernard Ladkin]

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

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
Styelfy Bleibgsnd
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200713/3d5efd15/attachment.sig>