[SystemSafety] Correctness by Construction

[Olwen Morgan]

That was the question on which I sought to focus the attention of the 
peeble-minded.

AFAI am aware from the use of SPARK Ada on a project on which I worked, 
it means, partial or, if your prover has the oomph for it, total 
correctness with respect to input and output predicates. Rod Chapman 
posted something explaining what the SPARK tools do. The capability of C 
tools varies and among open-source C tools those available from the 
FRAMA C project ( see link below) comprise a number of different 
verifiers that check different aspects of a C program's behaviour.

https://frama-c.com

Olwen



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