<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.E-MailFormatvorlage20
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:70.85pt 70.85pt 2.0cm 70.85pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:1963262106;
mso-list-template-ids:-1618035994;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link="#0563C1" vlink="#954F72"><div class=WordSection1><p class=MsoNormal>"Undecidable" means that there is no algorithm which can give a precise yes/no answer in every possible case. It does not mean you cannot prove the property. If you have a sound analyzer which does not report uninitialized variable accesses there are none. Unless there is a failure in the tool - which is why safety norms require tool qualification. In a sense, the purpose of a tool like Astrée is to check Rule 1.3. without false negatives.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Best regards,<o:p></o:p></p><p class=MsoNormal> Daniel.<o:p></o:p></p><p class=MsoNormal>---<o:p></o:p></p><div><p class=MsoNormal><span lang=DE>Dr.-Ing. Daniel Kaestner --------------------------------------------------------------------<br>AbsInt Angewandte Informatik GmbH Email: kaestner@AbsInt.com<br>Science Park 1 Tel: +49-681-3836028<br>66123 Saarbruecken Fax: +49-681-3836020<br>GERMANY </span><a href="http://www.absint.com/" target="_blank"><span lang=DE style='color:blue'>http://www.AbsInt.com</span></a><span lang=DE><br>----------------------------------------------------------------------------------------------------<br>Geschaeftsfuehrung: Dr.-Ing. </span>Christian Ferdinand<br>Eingetragen im Handelsregister des Amtsgerichts Saarbruecken, HRB 11234 <o:p></o:p></p><p class=MsoNormal> <o:p></o:p></p></div><p class=MsoNormal><o:p> </o:p></p><div><div style='border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm'><p class=MsoNormal><b><span lang=DE>Von:</span></b><span lang=DE> systemsafety <systemsafety-bounces@lists.techfak.uni-bielefeld.de> <b>Im Auftrag von </b>Roderick Chapman<br><b>Gesendet:</b> Mittwoch, 16. März 2022 14:22<br><b>An:</b> systemsafety@lists.techfak.uni-bielefeld.de<br><b>Betreff:</b> Re: [SystemSafety] Safety and programming languages<o:p></o:p></span></p></div></div><p class=MsoNormal><o:p> </o:p></p><div><p class=MsoNormal>On 16/03/2022 12:56, David Ward wrote:<o:p></o:p></p></div><blockquote style='margin-top:5.0pt;margin-bottom:5.0pt'><p class=MsoNormal style='mso-margin-top-alt:auto;mso-margin-bottom-alt:auto'><span style='font-size:10.0pt;font-family:"Arial",sans-serif;color:black'>Specifically</span><o:p></o:p></p><p class=MsoListParagraph style='margin-left:18.0pt;text-indent:-18.0pt;mso-list:l0 level1 lfo1'><![if !supportLists]><span style='font-size:10.0pt;font-family:Symbol;color:black'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'> </span></span></span><![endif]><span style='font-size:10.0pt;font-family:"Arial",sans-serif;color:black'>“System” is there because some guidelines can’t be checked at the software unit (or equivalent) level alone e.g. the one about recursions</span><span style='color:black'><o:p></o:p></span></p><p class=MsoListParagraph style='margin-left:18.0pt;text-indent:-18.0pt;mso-list:l0 level1 lfo1'><![if !supportLists]><span style='font-size:10.0pt;font-family:Symbol;color:black'><span style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'> </span></span></span><![endif]><span style='font-size:10.0pt;font-family:"Arial",sans-serif;color:black'>“Undecidable” is there because compliance to some guidelines cannot be demonstrated through static analysis alone and other methods are needed.</span><span style='color:black'><o:p></o:p></span></p></blockquote><p>I've applied a more pragmatic interpretation of those terms in the context of MISRA.<o:p></o:p></p><p>To me...<o:p></o:p></p><p>"System" means "this rule can't be checked on a single-translation unit, so it requires whole program analysis, which will be slow, and you'll only get really reliable results when you've finished the program, which is a bit late..."<o:p></o:p></p><p>"Undecideable" means "This rule is tough to check, so there will some mixture of false negatives and false positives. Exactly what you get depends on the whim of your chosen tool vendor..."<o:p></o:p></p><p>I also can't help noticing that all the _really_ important rules in MISRA are "System" and "Undecideable" - for example rules 1.3, 9.1, 13.2, 17.5 and 17.8 from MISRA 2012. Admitting false negatives for 1.3 ("don't have undefined behaviour") is particularly nasty, since any missed UB effectively undermines everything else.<o:p></o:p></p><p>SPARK and Rust both take a very different approach.<o:p></o:p></p><p> - Rod<o:p></o:p></p><p><o:p> </o:p></p></div></body></html>