[SystemSafety] Correctness by Construction
Olwen Morgan
olwen at phaedsys.com
Mon Jul 13 15:20:32 CEST 2020
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
More information about the systemsafety
mailing list